%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT350+2 : 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 : n009.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:11 AM UTC 2026
% Result : Theorem 48.23s 15.31s
% Output : Refutation 100.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 43
% Syntax : Number of formulae : 373 ( 71 unt; 6 def)
% Number of atoms : 2319 ( 214 equ)
% Maximal formula atoms : 26 ( 6 avg)
% Number of connectives : 3436 (1490 ~;1624 |; 252 &)
% ( 29 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 8 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 7 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 5 con; 0-5 aty)
% Number of variables : 594 ( 1 sgn 565 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f24,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f252,axiom,
! [X0,X1,X2] :
( r2_hidden(X0,k4_xboole_0(X1,k1_tarski(X2)))
<=> ( r2_hidden(X0,X1)
& X0 != X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t64_zfmisc_1) ).
fof(f253,axiom,
! [X0,X1] :
( k4_xboole_0(X0,k1_tarski(X1)) = X0
<=> ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f334,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
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/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f349,axiom,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset_1) ).
fof(f1257,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f1501,axiom,
! [X0] :
~ ( X0 != k1_xboole_0
& ! [X1] :
~ ( r2_hidden(X1,X0)
& ! [X2] :
( r2_hidden(X2,X1)
=> r1_xboole_0(X2,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_mcart_1) ).
fof(f1687,axiom,
! [X0,X1,X2,X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X1)
& m2_relset_1(X3,X0,X1) )
=> ( r1_tarski(X1,X2)
=> ( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_funct_2) ).
fof(f2965,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f5067,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f6009,axiom,
! [X0] :
( ( v4_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( r1_orders_2(X0,X1,X2)
& r1_orders_2(X0,X2,X1) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_orders_2) ).
fof(f6157,axiom,
! [X0] :
( l1_orders_2(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f6162,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& l1_orders_2(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( r3_orders_2(X0,X1,X2)
<=> r1_orders_2(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_orders_2) ).
fof(f6800,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ( v3_lattice3(X0)
=> ( v1_lattice3(X0)
& v2_lattice3(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_lattice3) ).
fof(f7410,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( r2_lattice3(X0,k1_xboole_0,X1)
& r1_lattice3(X0,k1_xboole_0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_yellow_0) ).
fof(f7444,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( X1 = k2_yellow_0(X0,X2)
<=> ( r1_lattice3(X0,X2,X1)
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r1_lattice3(X0,X2,X3)
=> r1_orders_2(X0,X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t33_yellow_0) ).
fof(f7456,axiom,
! [X0] :
( l1_orders_2(X0)
=> k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d12_yellow_0) ).
fof(f7495,axiom,
! [X0,X1] :
( l1_orders_2(X0)
=> m1_subset_1(k1_yellow_0(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f7498,axiom,
! [X0] :
( l1_orders_2(X0)
=> m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_yellow_0) ).
fof(f7662,axiom,
! [X0,X1,X2,X3] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& ~ v3_struct_0(X1)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_subset_1(X3,u1_struct_0(X0)) )
=> m1_subset_1(k1_waybel_0(X0,X1,X2,X3),u1_struct_0(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_waybel_0) ).
fof(f7663,axiom,
! [X0,X1,X2,X3] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& ~ v3_struct_0(X1)
& l1_struct_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
& m1_subset_1(X3,u1_struct_0(X0)) )
=> k1_waybel_0(X0,X1,X2,X3) = k1_funct_1(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_waybel_0) ).
fof(f7702,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k2_yellow_1(X0))
& v1_orders_2(k2_yellow_1(X0))
& v2_orders_2(k2_yellow_1(X0))
& v3_orders_2(k2_yellow_1(X0))
& v4_orders_2(k2_yellow_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_yellow_1) ).
fof(f7704,axiom,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc8_yellow_1) ).
fof(f7722,axiom,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_yellow_1) ).
fof(f7753,axiom,
! [X0] :
( v1_orders_2(k2_yellow_1(X0))
& l1_orders_2(k2_yellow_1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_yellow_1) ).
fof(f7793,axiom,
! [X0,X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& v3_lattice3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( r2_hidden(X2,X0)
=> ( r3_orders_2(X1,X2,k1_yellow_0(X1,X0))
& r3_orders_2(X1,k2_yellow_0(X1,X0),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t24_yellow_2) ).
fof(f8775,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ~ v1_xboole_0(k9_waybel_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_waybel16) ).
fof(f8793,axiom,
! [X0] : k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))) = k1_zfmisc_1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_waybel16) ).
fof(f8794,axiom,
! [X0] : k3_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_waybel16) ).
fof(f8947,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v3_struct_0(X2)
& v2_orders_2(X2)
& v3_orders_2(X2)
& v4_orders_2(X2)
& v3_lattice3(X2)
& v3_waybel_3(X2)
& l1_orders_2(X2)
& v1_funct_1(X3)
& v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
& m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
& m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) )
=> ( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(X1))
& X0 = k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5))
& r2_hidden(X5,X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_4_0_waybel22) ).
fof(f8948,axiom,
! [X0,X1,X2,X3,X4] :
( ( ~ v3_struct_0(X2)
& v2_orders_2(X2)
& v3_orders_2(X2)
& v4_orders_2(X2)
& v3_lattice3(X2)
& v3_waybel_3(X2)
& l1_orders_2(X2)
& v1_funct_1(X3)
& v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
& m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
& m1_subset_1(X4,k1_zfmisc_1(X1)) )
=> ( r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
& X0 = k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5))
& ? [X6] :
( m1_subset_1(X6,X1)
& X5 = k1_tarski(X6)
& r2_hidden(X6,X4) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fraenkel_a_4_1_waybel22) ).
fof(f8950,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
=> ( v1_funct_1(k2_waybel22(X0,X1,X2))
& v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
& m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_waybel22) ).
fof(f8968,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
=> ! [X3] :
( ( v1_funct_1(X3)
& v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
& m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
=> ( X3 = k2_waybel22(X0,X1,X2)
<=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))))
=> k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X4) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X4)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_waybel22) ).
fof(f8970,conjecture,
! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
=> k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) = k4_yellow_0(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_waybel22) ).
fof(f8971,negated_conjecture,
~ ! [X0,X1] :
( ( ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) )
=> ! [X2] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
=> k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) = k4_yellow_0(X1) ) ),
inference(negated_conjecture,[status(cth)],[f8970]) ).
fof(f8982,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f9022,plain,
? [X0,X1] :
( ? [X2] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) != k4_yellow_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) ),
inference(ennf_transformation,[],[f8971]) ).
fof(f9023,plain,
? [X0,X1] :
( ? [X2] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) != k4_yellow_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) ),
inference(flattening,[],[f9022]) ).
fof(f9026,plain,
! [X0] :
( ( v1_lattice3(X0)
& v2_lattice3(X0) )
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6800]) ).
fof(f9027,plain,
! [X0] :
( ( v1_lattice3(X0)
& v2_lattice3(X0) )
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9026]) ).
fof(f9038,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7498]) ).
fof(f9041,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7456]) ).
fof(f9044,plain,
! [X0,X1,X2,X3] :
( k1_waybel_0(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f7663]) ).
fof(f9045,plain,
! [X0,X1,X2,X3] :
( k1_waybel_0(X0,X1,X2,X3) = k1_funct_1(X2,X3)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(flattening,[],[f9044]) ).
fof(f9046,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k1_waybel_0(X0,X1,X2,X3),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f7662]) ).
fof(f9047,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k1_waybel_0(X0,X1,X2,X3),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(flattening,[],[f9046]) ).
fof(f9066,plain,
! [X0] :
( ~ v1_xboole_0(k9_waybel_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f8775]) ).
fof(f9067,plain,
! [X0] :
( ~ v1_xboole_0(k9_waybel_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9066]) ).
fof(f9077,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_waybel22(X0,X1,X2)
<=> ! [X4] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X4) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X4))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(ennf_transformation,[],[f8968]) ).
fof(f9078,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = k2_waybel22(X0,X1,X2)
<=> ! [X4] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X4) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X4))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(flattening,[],[f9077]) ).
fof(f9079,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel22(X0,X1,X2))
& v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
& m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(ennf_transformation,[],[f8950]) ).
fof(f9080,plain,
! [X0,X1,X2] :
( ( v1_funct_1(k2_waybel22(X0,X1,X2))
& v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
& m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(flattening,[],[f9079]) ).
fof(f9097,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_orders_2(X0,X1,X2)
| ~ r1_orders_2(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6009]) ).
fof(f9098,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_orders_2(X0,X1,X2)
| ~ r1_orders_2(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9097]) ).
fof(f9171,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(f9228,plain,
! [X0,X1,X2,X3] :
( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(X1,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(ennf_transformation,[],[f1687]) ).
fof(f9229,plain,
! [X0,X1,X2,X3] :
( ( X1 = k1_xboole_0
& X0 != k1_xboole_0 )
| ( v1_funct_1(X3)
& v1_funct_2(X3,X0,X2)
& m2_relset_1(X3,X0,X2) )
| ~ r1_tarski(X1,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(flattening,[],[f9228]) ).
fof(f9257,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f6157]) ).
fof(f9261,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f5067]) ).
fof(f9262,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f9261]) ).
fof(f9263,plain,
! [X0] :
( ( ~ v3_struct_0(k2_yellow_1(X0))
& v1_orders_2(k2_yellow_1(X0))
& v2_orders_2(k2_yellow_1(X0))
& v3_orders_2(k2_yellow_1(X0))
& v4_orders_2(k2_yellow_1(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f7702]) ).
fof(f9304,plain,
! [X0,X1] :
( m1_subset_1(k1_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7495]) ).
fof(f9573,plain,
! [X0,X1] :
( ! [X2] :
( ( r3_orders_2(X1,X2,k1_yellow_0(X1,X0))
& r3_orders_2(X1,k2_yellow_0(X1,X0),X2) )
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) ),
inference(ennf_transformation,[],[f7793]) ).
fof(f9574,plain,
! [X0,X1] :
( ! [X2] :
( ( r3_orders_2(X1,X2,k1_yellow_0(X1,X0))
& r3_orders_2(X1,k2_yellow_0(X1,X0),X2) )
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X2,u1_struct_0(X1)) )
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) ),
inference(flattening,[],[f9573]) ).
fof(f9576,plain,
! [X0,X1,X2] :
( ( r3_orders_2(X0,X1,X2)
<=> r1_orders_2(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f6162]) ).
fof(f9577,plain,
! [X0,X1,X2] :
( ( r3_orders_2(X0,X1,X2)
<=> r1_orders_2(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f9576]) ).
fof(f9595,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(X1))
& X0 = k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5))
& r2_hidden(X5,X4) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(ennf_transformation,[],[f8947]) ).
fof(f9596,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(X1))
& X0 = k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5))
& r2_hidden(X5,X4) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(flattening,[],[f9595]) ).
fof(f9615,plain,
! [X0] :
( k1_xboole_0 = X0
| ? [X1] :
( r2_hidden(X1,X0)
& ! [X2] :
( r1_xboole_0(X2,X0)
| ~ r2_hidden(X2,X1) ) ) ),
inference(ennf_transformation,[],[f1501]) ).
fof(f9878,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = k2_yellow_0(X0,X2)
<=> ( r1_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X3,X1)
| ~ r1_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7444]) ).
fof(f9879,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = k2_yellow_0(X0,X2)
<=> ( r1_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X3,X1)
| ~ r1_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f9878]) ).
fof(f9897,plain,
! [X0] :
( ! [X1] :
( ( r2_lattice3(X0,k1_xboole_0,X1)
& r1_lattice3(X0,k1_xboole_0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f7410]) ).
fof(f10192,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
& X0 = k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5))
& ? [X6] :
( m1_subset_1(X6,X1)
& X5 = k1_tarski(X6)
& r2_hidden(X6,X4) ) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1)) ),
inference(ennf_transformation,[],[f8948]) ).
fof(f10193,plain,
! [X0,X1,X2,X3,X4] :
( ( r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
<=> ? [X5] :
( m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
& X0 = k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5))
& ? [X6] :
( m1_subset_1(X6,X1)
& X5 = k1_tarski(X6)
& r2_hidden(X6,X4) ) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1)) ),
inference(flattening,[],[f10192]) ).
fof(f10807,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK54))),sK55,k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK54))))) != k4_yellow_0(sK55)
& v1_funct_1(sK56)
& v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
& m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
& ~ v3_struct_0(sK55)
& v2_orders_2(sK55)
& v3_orders_2(sK55)
& v4_orders_2(sK55)
& v3_lattice3(sK55)
& v3_waybel_3(sK55)
& l1_orders_2(sK55) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54,sK55,sK56]),skolemize(X0,sK54),skolemize(X1,sK55),skolemize(X2,sK56)],[f9023]) ).
fof(f10817,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_waybel22(X0,X1,X2)
| ? [X4] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X4) != k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X4))
& m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) ) )
& ( ! [X4] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X4) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X4))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) )
| k2_waybel22(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(nnf_transformation,[],[f9078]) ).
fof(f10818,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_waybel22(X0,X1,X2)
| ? [X4] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X4) != k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X4))
& m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) ) )
& ( ! [X5] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X5) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X5))
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) )
| k2_waybel22(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(rectify,[],[f10817]) ).
fof(f10819,plain,
! [X0,X1] :
( ! [X2] :
( ! [X3] :
( ( ( X3 = k2_waybel22(X0,X1,X2)
| ( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,sK64(X0,X1,X2,X3)) != k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,sK64(X0,X1,X2,X3)))
& m1_subset_1(sK64(X0,X1,X2,X3),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) ) )
& ( ! [X5] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X5) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X5))
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) )
| k2_waybel22(X0,X1,X2) != X3 ) )
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1)) )
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64]),skolemize(X4,sK64(X0,X1,X2,X3))],[f10818]) ).
fof(f10848,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,[],[f9171]) ).
fof(f10914,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f10915,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f10914]) ).
fof(f10916,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK126(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK126]),skolemize(X1,sK126(X0))],[f10915]) ).
fof(f10921,plain,
! [X0,X1,X2] :
( ( m2_relset_1(X2,X0,X1)
| ~ m1_relset_1(X2,X0,X1) )
& ( m1_relset_1(X2,X0,X1)
| ~ m2_relset_1(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f1257]) ).
fof(f11056,plain,
! [X0,X1,X2] :
( ( ( r3_orders_2(X0,X1,X2)
| ~ r1_orders_2(X0,X1,X2) )
& ( r1_orders_2(X0,X1,X2)
| ~ r3_orders_2(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(nnf_transformation,[],[f9577]) ).
fof(f11073,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(X1))
| k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5)) != X0
| ~ r2_hidden(X5,X4) ) )
& ( ? [X5] :
( m1_subset_1(X5,k1_zfmisc_1(X1))
& X0 = k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5))
& r2_hidden(X5,X4) )
| ~ r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4)) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(nnf_transformation,[],[f9596]) ).
fof(f11074,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(X1))
| k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5)) != X0
| ~ r2_hidden(X5,X4) ) )
& ( ? [X6] :
( m1_subset_1(X6,k1_zfmisc_1(X1))
& k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X6)) = X0
& r2_hidden(X6,X4) )
| ~ r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4)) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(rectify,[],[f11073]) ).
fof(f11075,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,k1_zfmisc_1(X1))
| k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5)) != X0
| ~ r2_hidden(X5,X4) ) )
& ( ( m1_subset_1(sK196(X0,X1,X2,X3,X4),k1_zfmisc_1(X1))
& k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,sK196(X0,X1,X2,X3,X4))) = X0
& r2_hidden(sK196(X0,X1,X2,X3,X4),X4) )
| ~ r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4)) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK196]),skolemize(X6,sK196(X0,X1,X2,X3,X4))],[f11074]) ).
fof(f11088,plain,
! [X0] :
( k1_xboole_0 = X0
| ( r2_hidden(sK210(X0),X0)
& ! [X2] :
( r1_xboole_0(X2,X0)
| ~ r2_hidden(X2,sK210(X0)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK210]),skolemize(X1,sK210(X0))],[f9615]) ).
fof(f11227,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k2_yellow_0(X0,X2)
| ~ r1_lattice3(X0,X2,X1)
| ? [X3] :
( ~ r1_orders_2(X0,X3,X1)
& r1_lattice3(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r1_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X3,X1)
| ~ r1_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k2_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f9879]) ).
fof(f11228,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k2_yellow_0(X0,X2)
| ~ r1_lattice3(X0,X2,X1)
| ? [X3] :
( ~ r1_orders_2(X0,X3,X1)
& r1_lattice3(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r1_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X3,X1)
| ~ r1_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k2_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f11227]) ).
fof(f11229,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k2_yellow_0(X0,X2)
| ~ r1_lattice3(X0,X2,X1)
| ? [X3] :
( ~ r1_orders_2(X0,X3,X1)
& r1_lattice3(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r1_lattice3(X0,X2,X1)
& ! [X4] :
( r1_orders_2(X0,X4,X1)
| ~ r1_lattice3(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k2_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f11228]) ).
fof(f11230,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k2_yellow_0(X0,X2)
| ~ r1_lattice3(X0,X2,X1)
| ( ~ r1_orders_2(X0,sK314(X0,X1,X2),X1)
& r1_lattice3(X0,X2,sK314(X0,X1,X2))
& m1_subset_1(sK314(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ( r1_lattice3(X0,X2,X1)
& ! [X4] :
( r1_orders_2(X0,X4,X1)
| ~ r1_lattice3(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k2_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK314]),skolemize(X3,sK314(X0,X1,X2))],[f11229]) ).
fof(f11363,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
| k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5)) != X0
| ! [X6] :
( ~ m1_subset_1(X6,X1)
| k1_tarski(X6) != X5
| ~ r2_hidden(X6,X4) ) ) )
& ( ? [X5] :
( m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
& X0 = k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5))
& ? [X6] :
( m1_subset_1(X6,X1)
& X5 = k1_tarski(X6)
& r2_hidden(X6,X4) ) )
| ~ r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4)) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1)) ),
inference(nnf_transformation,[],[f10193]) ).
fof(f11364,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
| k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5)) != X0
| ! [X6] :
( ~ m1_subset_1(X6,X1)
| k1_tarski(X6) != X5
| ~ r2_hidden(X6,X4) ) ) )
& ( ? [X7] :
( m1_subset_1(X7,u1_struct_0(k3_yellow_1(X1)))
& k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X7)) = X0
& ? [X8] :
( m1_subset_1(X8,X1)
& k1_tarski(X8) = X7
& r2_hidden(X8,X4) ) )
| ~ r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4)) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1)) ),
inference(rectify,[],[f11363]) ).
fof(f11365,plain,
! [X0,X1,X2,X3,X4] :
( ( ( r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
| ! [X5] :
( ~ m1_subset_1(X5,u1_struct_0(k3_yellow_1(X1)))
| k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),X5)) != X0
| ! [X6] :
( ~ m1_subset_1(X6,X1)
| k1_tarski(X6) != X5
| ~ r2_hidden(X6,X4) ) ) )
& ( ( m1_subset_1(sK389(X0,X1,X3,X4),u1_struct_0(k3_yellow_1(X1)))
& k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),sK389(X0,X1,X3,X4))) = X0
& m1_subset_1(sK390(X0,X1,X3,X4),X1)
& sK389(X0,X1,X3,X4) = k1_tarski(sK390(X0,X1,X3,X4))
& r2_hidden(sK390(X0,X1,X3,X4),X4) )
| ~ r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4)) ) )
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK389,sK390]),skolemize(X7,sK389(X0,X1,X3,X4)),skolemize(X8,sK390(X0,X1,X3,X4))],[f11364]) ).
fof(f11389,plain,
! [X0,X1] :
( ( k4_xboole_0(X0,k1_tarski(X1)) = X0
| r2_hidden(X1,X0) )
& ( ~ r2_hidden(X1,X0)
| k4_xboole_0(X0,k1_tarski(X1)) != X0 ) ),
inference(nnf_transformation,[],[f253]) ).
fof(f11390,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k4_xboole_0(X1,k1_tarski(X2)))
| ~ r2_hidden(X0,X1)
| X0 = X2 )
& ( ( r2_hidden(X0,X1)
& X0 != X2 )
| ~ r2_hidden(X0,k4_xboole_0(X1,k1_tarski(X2))) ) ),
inference(nnf_transformation,[],[f252]) ).
fof(f11391,plain,
! [X0,X1,X2] :
( ( r2_hidden(X0,k4_xboole_0(X1,k1_tarski(X2)))
| ~ r2_hidden(X0,X1)
| X0 = X2 )
& ( ( r2_hidden(X0,X1)
& X0 != X2 )
| ~ r2_hidden(X0,k4_xboole_0(X1,k1_tarski(X2))) ) ),
inference(flattening,[],[f11390]) ).
fof(f11545,plain,
l1_orders_2(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11546,plain,
v3_waybel_3(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11547,plain,
v3_lattice3(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11548,plain,
v4_orders_2(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11549,plain,
v3_orders_2(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11550,plain,
v2_orders_2(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11551,plain,
~ v3_struct_0(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11552,plain,
m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)),
inference(cnf_transformation,[],[f10807]) ).
fof(f11553,plain,
v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55)),
inference(cnf_transformation,[],[f10807]) ).
fof(f11554,plain,
v1_funct_1(sK56),
inference(cnf_transformation,[],[f10807]) ).
fof(f11555,plain,
k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK54))),sK55,k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK54))))) != k4_yellow_0(sK55),
inference(cnf_transformation,[],[f10807]) ).
fof(f11561,plain,
! [X0] :
( ~ v3_lattice3(X0)
| v2_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9027]) ).
fof(f11562,plain,
! [X0] :
( ~ v3_lattice3(X0)
| v1_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9027]) ).
fof(f11569,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9038]) ).
fof(f11571,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9041]) ).
fof(f11574,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| k1_funct_1(X2,X3) = k1_waybel_0(X0,X1,X2,X3)
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f9045]) ).
fof(f11575,plain,
! [X2,X3,X0,X1] :
( m1_subset_1(k1_waybel_0(X0,X1,X2,X3),u1_struct_0(X1))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f9047]) ).
fof(f11594,plain,
! [X0] : k1_tarski(X0) = k3_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),
inference(cnf_transformation,[],[f8794]) ).
fof(f11595,plain,
! [X0] : k1_zfmisc_1(X0) = k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),
inference(cnf_transformation,[],[f8793]) ).
fof(f11617,plain,
! [X0] :
( ~ v1_xboole_0(k9_waybel_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9067]) ).
fof(f11639,plain,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f7722]) ).
fof(f11651,plain,
! [X2,X3,X0,X1,X5] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,X3,X5) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X5))
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))))
| k2_waybel22(X0,X1,X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(cnf_transformation,[],[f10819]) ).
fof(f11654,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f9080]) ).
fof(f11655,plain,
! [X2,X0,X1] :
( v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f9080]) ).
fof(f11656,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| v1_funct_1(k2_waybel22(X0,X1,X2))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f9080]) ).
fof(f11703,plain,
! [X2,X0,X1] :
( ~ r1_orders_2(X0,X2,X1)
| ~ r1_orders_2(X0,X1,X2)
| X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9098]) ).
fof(f11771,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f10848]) ).
fof(f11791,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f334]) ).
fof(f11924,plain,
! [X2,X3,X0,X1] :
( k1_xboole_0 = X1
| v1_funct_2(X3,X0,X2)
| ~ r1_tarski(X1,X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,X0,X1)
| ~ m2_relset_1(X3,X0,X1) ),
inference(cnf_transformation,[],[f9229]) ).
fof(f11939,plain,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f349]) ).
fof(f11945,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f10916]) ).
fof(f11947,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f24]) ).
fof(f11967,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f10921]) ).
fof(f11972,plain,
! [X0] :
( ~ l1_orders_2(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f9257]) ).
fof(f11978,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f9262]) ).
fof(f11981,plain,
! [X0] : l1_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f7753]) ).
fof(f11987,plain,
! [X0] :
( ~ v3_struct_0(k2_yellow_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f9263]) ).
fof(f12040,plain,
! [X0] : v2_yellow_0(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f7704]) ).
fof(f12042,plain,
! [X0] : v4_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f7704]) ).
fof(f12043,plain,
! [X0] : v3_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f7704]) ).
fof(f12044,plain,
! [X0] : v2_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f7704]) ).
fof(f12046,plain,
! [X0] : ~ v3_struct_0(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f7704]) ).
fof(f12168,plain,
! [X0,X1] :
( m1_subset_1(k1_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9304]) ).
fof(f12541,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f8982]) ).
fof(f12593,plain,
! [X2,X0,X1] :
( r3_orders_2(X1,X2,k1_yellow_0(X1,X0))
| ~ r2_hidden(X2,X0)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1) ),
inference(cnf_transformation,[],[f9574]) ).
fof(f12596,plain,
! [X2,X0,X1] :
( ~ r3_orders_2(X0,X1,X2)
| r1_orders_2(X0,X1,X2)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f11056]) ).
fof(f12641,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
| ~ m1_subset_1(X5,k1_zfmisc_1(X1))
| k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5)) != X0
| ~ r2_hidden(X5,X4)
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(cnf_transformation,[],[f11075]) ).
fof(f12678,plain,
! [X0] :
( k1_xboole_0 = X0
| r2_hidden(sK210(X0),X0) ),
inference(cnf_transformation,[],[f11088]) ).
fof(f13111,plain,
! [X2,X0,X1,X4] :
( r1_orders_2(X0,X4,X1)
| ~ r1_lattice3(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| k2_yellow_0(X0,X2) != X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f11230]) ).
fof(f13167,plain,
! [X0,X1] :
( r1_lattice3(X0,k1_xboole_0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f9897]) ).
fof(f13676,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
| r2_hidden(sK390(X0,X1,X3,X4),X4)
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[],[f11365]) ).
fof(f13810,plain,
! [X0,X1] :
( k4_xboole_0(X0,k1_tarski(X1)) = X0
| r2_hidden(X1,X0) ),
inference(cnf_transformation,[],[f11389]) ).
fof(f13811,plain,
! [X2,X0,X1] :
( X0 != X2
| ~ r2_hidden(X0,k4_xboole_0(X1,k1_tarski(X2))) ),
inference(cnf_transformation,[],[f11391]) ).
fof(f14219,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f2965]) ).
fof(f14405,plain,
! [X0] : k1_tarski(X0) = k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),
inference(definition_unfolding,[],[f11594,f11639]) ).
fof(f14407,plain,
! [X0] : k1_zfmisc_1(X0) = k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),
inference(definition_unfolding,[],[f11595,f11639]) ).
fof(f14408,plain,
k4_yellow_0(sK55) != k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))),
inference(definition_unfolding,[],[f11555,f11639,f11639]) ).
fof(f14410,plain,
! [X0] :
( ~ l1_orders_2(X0)
| k4_yellow_0(X0) = k2_yellow_0(X0,np__0) ),
inference(definition_unfolding,[],[f11571,f14219]) ).
fof(f14447,plain,
! [X2,X3,X0,X1,X5] :
( k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X5)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,X3,X5)
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))))
| k2_waybel22(X0,X1,X2) != X3
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| ~ m2_relset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(definition_unfolding,[],[f11651,f11639,f11639,f11639,f11639]) ).
fof(f14448,plain,
! [X2,X0,X1] :
( v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(definition_unfolding,[],[f11655,f11639]) ).
fof(f14449,plain,
! [X2,X0,X1] :
( m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(definition_unfolding,[],[f11654,f11639]) ).
fof(f14477,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_2(X3,X0,X1)
| v1_funct_2(X3,X0,X2)
| ~ r1_tarski(X1,X2)
| ~ v1_funct_1(X3)
| np__0 = X1
| ~ m2_relset_1(X3,X0,X1) ),
inference(definition_unfolding,[],[f11924,f14219]) ).
fof(f14495,plain,
! [X0] : m1_subset_1(np__0,k1_zfmisc_1(X0)),
inference(definition_unfolding,[],[f11939,f14219]) ).
fof(f14502,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| np__0 != X0 ),
inference(definition_unfolding,[],[f11945,f14219]) ).
fof(f14503,plain,
v1_xboole_0(np__0),
inference(definition_unfolding,[],[f11947,f14219]) ).
fof(f14505,plain,
! [X0] : ~ v3_struct_0(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f12046,f11639]) ).
fof(f14507,plain,
! [X0] : v2_orders_2(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f12044,f11639]) ).
fof(f14508,plain,
! [X0] : v3_orders_2(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f12043,f11639]) ).
fof(f14509,plain,
! [X0] : v4_orders_2(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f12042,f11639]) ).
fof(f14511,plain,
! [X0] : v2_yellow_0(k2_yellow_1(k1_zfmisc_1(X0))),
inference(definition_unfolding,[],[f12040,f11639]) ).
fof(f14700,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
| ~ m1_subset_1(X5,k1_zfmisc_1(X1))
| k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5)) != X0
| ~ r2_hidden(X5,X4)
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))) ),
inference(definition_unfolding,[],[f12641,f11639]) ).
fof(f14722,plain,
! [X0] :
( r2_hidden(sK210(X0),X0)
| np__0 = X0 ),
inference(definition_unfolding,[],[f12678,f14219]) ).
fof(f14908,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| r1_lattice3(X0,np__0,X1)
| ~ l1_orders_2(X0) ),
inference(definition_unfolding,[],[f13167,f14219]) ).
fof(f15105,plain,
! [X0,X1] :
( r2_hidden(X1,X0)
| k4_xboole_0(X0,k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))) = X0 ),
inference(definition_unfolding,[],[f13810,f14405]) ).
fof(f15109,plain,
! [X2,X0,X1] :
( X0 != X2
| ~ r2_hidden(X0,k4_xboole_0(X1,k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))) ),
inference(definition_unfolding,[],[f13811,f14405]) ).
fof(f15322,plain,
! [X2,X0,X1,X5] :
( ~ v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))))
| ~ v1_funct_1(k2_waybel22(X0,X1,X2))
| k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X5)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),X5)
| ~ m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1) ),
inference(equality_resolution,[],[f14447]) ).
fof(f15334,plain,
! [X2] : ~ r2_hidden(X2,np__0),
inference(equality_resolution,[],[f14502]) ).
fof(f15373,plain,
! [X2,X3,X1,X4,X5] :
( r2_hidden(k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,X5)),a_4_0_waybel22(X1,X2,X3,X4))
| ~ m1_subset_1(X5,k1_zfmisc_1(X1))
| ~ r2_hidden(X5,X4)
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ v3_waybel_3(X2)
| ~ l1_orders_2(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))) ),
inference(equality_resolution,[],[f14700]) ).
fof(f15401,plain,
! [X2,X0,X4] :
( ~ m1_subset_1(k2_yellow_0(X0,X2),u1_struct_0(X0))
| ~ r1_lattice3(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| r1_orders_2(X0,X4,k2_yellow_0(X0,X2))
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f13111]) ).
fof(f15468,plain,
! [X2,X1] : ~ r2_hidden(X2,k4_xboole_0(X1,k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))),
inference(equality_resolution,[],[f15109]) ).
fof(f15699,plain,
m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)),
inference(resolution,[],[f11967,f11552]) ).
fof(f15702,plain,
k4_yellow_0(sK55) = k2_yellow_0(sK55,np__0),
inference(resolution,[],[f14410,f11545]) ).
fof(f15703,plain,
( v3_struct_0(sK55)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(resolution,[],[f11656,f11553]) ).
fof(f15704,plain,
( ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15703,f11551]) ).
fof(f15705,plain,
( ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15704,f11550]) ).
fof(f15706,plain,
( ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15705,f11549]) ).
fof(f15707,plain,
( ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15706,f11548]) ).
fof(f15708,plain,
( ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15707,f11547]) ).
fof(f15709,plain,
( ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15708,f11546]) ).
fof(f15710,plain,
( ~ v1_funct_1(sK56)
| v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15709,f11545]) ).
fof(f15711,plain,
( v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f15710,f11554]) ).
fof(f15712,plain,
v1_funct_1(k2_waybel22(sK54,sK55,sK56)),
inference(forward_subsumption_resolution,[],[f15711,f15699]) ).
fof(f15717,plain,
! [X2,X0,X1] :
( m1_relset_1(k2_waybel22(X2,X0,X1),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(resolution,[],[f14449,f11967]) ).
fof(f15723,plain,
l1_struct_0(sK55),
inference(resolution,[],[f11972,f11545]) ).
fof(f15755,plain,
k4_yellow_0(sK55) != k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),
inference(superposition,[],[f14408,f14407]) ).
fof(f15757,plain,
! [X0] :
( m1_subset_1(k1_zfmisc_1(X0),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))))
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(superposition,[],[f11569,f14407]) ).
fof(f15758,plain,
! [X0] : m1_subset_1(k1_zfmisc_1(X0),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))),
inference(forward_subsumption_resolution,[],[f15757,f11981]) ).
fof(f15898,definition,
( spl481_16
<=> np__0 = u1_struct_0(sK55) ),
introduced(definition,[new_symbols(definition,[spl481_16])],[avatar_definition]) ).
fof(f15899,plain,
( np__0 != u1_struct_0(sK55)
| spl481_16 ),
inference(avatar_component_clause,[],[f15898]) ).
fof(f15900,plain,
( np__0 = u1_struct_0(sK55)
| ~ spl481_16 ),
inference(avatar_component_clause,[],[f15898]) ).
fof(f15918,plain,
( ~ v1_xboole_0(np__0)
| v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ spl481_16 ),
inference(superposition,[],[f11978,f15900]) ).
fof(f15937,plain,
( v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ spl481_16 ),
inference(forward_subsumption_resolution,[],[f15918,f14503]) ).
fof(f15955,plain,
( ~ l1_struct_0(sK55)
| ~ spl481_16 ),
inference(forward_subsumption_resolution,[],[f15937,f11551]) ).
fof(f15969,plain,
( $false
| ~ spl481_16 ),
inference(forward_subsumption_resolution,[],[f15955,f15723]) ).
fof(f15970,plain,
~ spl481_16,
inference(avatar_contradiction_clause,[],[f15969]) ).
fof(f16016,plain,
! [X0] : l1_struct_0(k2_yellow_1(X0)),
inference(resolution,[],[f11981,f11972]) ).
fof(f16146,plain,
! [X2,X3,X0,X1] :
( v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),X3)
| ~ r1_tarski(u1_struct_0(X1),X3)
| ~ v1_funct_1(k2_waybel22(X0,X1,X2))
| np__0 = u1_struct_0(X1)
| ~ m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(resolution,[],[f14477,f14448]) ).
fof(f16150,plain,
! [X2,X3,X0,X1] :
( v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),X3)
| ~ r1_tarski(u1_struct_0(X1),X3)
| np__0 = u1_struct_0(X1)
| ~ m2_relset_1(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f16146,f11656]) ).
fof(f16152,plain,
! [X2,X3,X0,X1] :
( v1_funct_2(k2_waybel22(X0,X1,X2),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))),X3)
| ~ r1_tarski(u1_struct_0(X1),X3)
| np__0 = u1_struct_0(X1)
| v3_struct_0(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ v3_waybel_3(X1)
| ~ l1_orders_2(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f16150,f14449]) ).
fof(f16615,plain,
! [X0] :
( r2_hidden(np__0,k1_zfmisc_1(X0))
| v1_xboole_0(k1_zfmisc_1(X0)) ),
inference(resolution,[],[f11771,f14495]) ).
fof(f16632,plain,
! [X0] : r2_hidden(np__0,k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[],[f16615,f11791]) ).
fof(f17497,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2)
| ~ v2_lattice3(X2)
| ~ v3_lattice3(X2)
| ~ l1_orders_2(X2)
| r1_orders_2(X2,X0,k1_yellow_0(X2,X1))
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ l1_orders_2(X2)
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ m1_subset_1(k1_yellow_0(X2,X1),u1_struct_0(X2)) ),
inference(resolution,[],[f12593,f12596]) ).
fof(f17500,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v1_lattice3(X2)
| ~ v2_lattice3(X2)
| ~ v3_lattice3(X2)
| ~ l1_orders_2(X2)
| r1_orders_2(X2,X0,k1_yellow_0(X2,X1))
| v3_struct_0(X2)
| ~ m1_subset_1(k1_yellow_0(X2,X1),u1_struct_0(X2)) ),
inference(duplicate_literal_removal,[],[f17497]) ).
fof(f17501,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v2_lattice3(X2)
| ~ v3_lattice3(X2)
| ~ l1_orders_2(X2)
| r1_orders_2(X2,X0,k1_yellow_0(X2,X1))
| v3_struct_0(X2)
| ~ m1_subset_1(k1_yellow_0(X2,X1),u1_struct_0(X2)) ),
inference(forward_subsumption_resolution,[],[f17500,f11562]) ).
fof(f17502,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ l1_orders_2(X2)
| r1_orders_2(X2,X0,k1_yellow_0(X2,X1))
| v3_struct_0(X2)
| ~ m1_subset_1(k1_yellow_0(X2,X1),u1_struct_0(X2)) ),
inference(forward_subsumption_resolution,[],[f17501,f11561]) ).
fof(f17503,plain,
! [X2,X0,X1] :
( r1_orders_2(X2,X0,k1_yellow_0(X2,X1))
| ~ m1_subset_1(X0,u1_struct_0(X2))
| ~ v2_orders_2(X2)
| ~ v3_orders_2(X2)
| ~ v4_orders_2(X2)
| ~ v3_lattice3(X2)
| ~ l1_orders_2(X2)
| ~ r2_hidden(X0,X1)
| v3_struct_0(X2) ),
inference(forward_subsumption_resolution,[],[f17502,f12168]) ).
fof(f17506,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r2_hidden(X0,X2)
| v3_struct_0(X1)
| ~ r1_orders_2(X1,k1_yellow_0(X1,X2),X0)
| k1_yellow_0(X1,X2) = X0
| ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ m1_subset_1(k1_yellow_0(X1,X2),u1_struct_0(X1))
| ~ v4_orders_2(X1)
| ~ l1_orders_2(X1) ),
inference(resolution,[],[f17503,f11703]) ).
fof(f17511,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(X1))
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r2_hidden(X0,X2)
| v3_struct_0(X1)
| ~ r1_orders_2(X1,k1_yellow_0(X1,X2),X0)
| k1_yellow_0(X1,X2) = X0
| ~ m1_subset_1(k1_yellow_0(X1,X2),u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f17506]) ).
fof(f17515,plain,
! [X2,X0,X1] :
( ~ r1_orders_2(X1,k1_yellow_0(X1,X2),X0)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v3_lattice3(X1)
| ~ l1_orders_2(X1)
| ~ r2_hidden(X0,X2)
| v3_struct_0(X1)
| ~ m1_subset_1(X0,u1_struct_0(X1))
| k1_yellow_0(X1,X2) = X0 ),
inference(forward_subsumption_resolution,[],[f17511,f12168]) ).
fof(f19621,plain,
! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK55),u1_struct_0(sK55))
| ~ r1_lattice3(sK55,np__0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK55))
| r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| v3_struct_0(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55) ),
inference(superposition,[],[f15401,f15702]) ).
fof(f19653,plain,
! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK55),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(sK55))
| r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| v3_struct_0(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55) ),
inference(forward_subsumption_resolution,[],[f19621,f14908]) ).
fof(f19669,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK55))
| r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| v3_struct_0(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55) ),
inference(forward_subsumption_resolution,[],[f19653,f11569]) ).
fof(f19685,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK55))
| r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55) ),
inference(forward_subsumption_resolution,[],[f19669,f11551]) ).
fof(f19701,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK55))
| r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55) ),
inference(forward_subsumption_resolution,[],[f19685,f11548]) ).
fof(f19717,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK55))
| r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| ~ l1_orders_2(sK55) ),
inference(forward_subsumption_resolution,[],[f19701,f11547]) ).
fof(f19725,plain,
! [X0] :
( r1_orders_2(sK55,X0,k4_yellow_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f19717,f11545]) ).
fof(f19741,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55)
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| ~ m1_subset_1(k4_yellow_0(sK55),u1_struct_0(sK55))
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(resolution,[],[f19725,f17515]) ).
fof(f19750,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55)
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19741,f11569]) ).
fof(f19764,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55)
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19750,f11550]) ).
fof(f19769,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55)
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19764,f11549]) ).
fof(f19774,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ v3_lattice3(sK55)
| ~ l1_orders_2(sK55)
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19769,f11548]) ).
fof(f19776,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ l1_orders_2(sK55)
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19774,f11547]) ).
fof(f19777,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| v3_struct_0(sK55)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19776,f11545]) ).
fof(f19778,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK55,X0),u1_struct_0(sK55))
| ~ r2_hidden(k4_yellow_0(sK55),X0)
| k4_yellow_0(sK55) = k1_yellow_0(sK55,X0) ),
inference(forward_subsumption_resolution,[],[f19777,f11551]) ).
fof(f20283,plain,
! [X2,X3,X0,X1,X4] :
( ~ v1_funct_2(X2,k1_waybel22(X1),u1_struct_0(X4))
| v3_struct_0(X4)
| ~ v2_orders_2(X4)
| ~ v3_orders_2(X4)
| ~ v4_orders_2(X4)
| ~ v3_lattice3(X4)
| ~ v3_waybel_3(X4)
| ~ l1_orders_2(X4)
| ~ v1_funct_1(X2)
| r2_hidden(sK390(X0,X1,X2,X3),X3)
| ~ m2_relset_1(X2,k1_waybel22(X1),u1_struct_0(X4))
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| a_4_1_waybel22(X1,X4,X2,X3) = k4_xboole_0(a_4_1_waybel22(X1,X4,X2,X3),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(resolution,[],[f13676,f15105]) ).
fof(f21229,plain,
! [X2,X3,X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))
| ~ v1_funct_1(k2_waybel22(X2,X0,X1))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),X3) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,X3))
| ~ m2_relset_1(k2_waybel22(X2,X0,X1),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))),u1_struct_0(X0))
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f16152,f15322]) ).
fof(f21250,plain,
! [X2,X3,X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))
| ~ v1_funct_1(k2_waybel22(X2,X0,X1))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),X3) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,X3))
| ~ m2_relset_1(k2_waybel22(X2,X0,X1),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(duplicate_literal_removal,[],[f21229]) ).
fof(f21271,plain,
! [X2,X3,X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),X3) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,X3))
| ~ m2_relset_1(k2_waybel22(X2,X0,X1),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))),u1_struct_0(X0))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f21250,f11656]) ).
fof(f21291,plain,
! [X2,X3,X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),X3) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,X3))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f21271,f14449]) ).
fof(f21295,plain,
! [X2,X3,X0,X1] :
( ~ r1_tarski(u1_struct_0(X0),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),X3) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,X3))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f21291,f11967]) ).
fof(f21296,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),X3) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,X3))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f21295,f12541]) ).
fof(f21300,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0))
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2))))) ),
inference(resolution,[],[f21296,f11569]) ).
fof(f21309,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| np__0 = u1_struct_0(X0)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))))
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(forward_subsumption_resolution,[],[f21300,f11981]) ).
fof(f21313,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X1,k1_waybel22(X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))),X0,k2_waybel22(X2,X0,X1),k1_zfmisc_1(X2)) = k1_yellow_0(X0,a_4_0_waybel22(X2,X0,X1,k1_zfmisc_1(X2)))
| np__0 = u1_struct_0(X0)
| ~ m2_relset_1(X1,k1_waybel22(X2),u1_struct_0(X0)) ),
inference(forward_demodulation,[],[f21309,f14407]) ).
fof(f22021,plain,
! [X0,X1] :
( v3_struct_0(sK55)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(resolution,[],[f20283,f11553]) ).
fof(f22026,plain,
! [X0,X1] :
( ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22021,f11551]) ).
fof(f22029,plain,
! [X0,X1] :
( ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22026,f11550]) ).
fof(f22030,plain,
! [X0,X1] :
( ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22029,f11549]) ).
fof(f22031,plain,
! [X0,X1] :
( ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22030,f11548]) ).
fof(f22032,plain,
! [X0,X1] :
( ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22031,f11547]) ).
fof(f22033,plain,
! [X0,X1] :
( ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22032,f11546]) ).
fof(f22034,plain,
! [X0,X1] :
( ~ v1_funct_1(sK56)
| r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22033,f11545]) ).
fof(f22035,plain,
! [X0,X1] :
( r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22034,f11554]) ).
fof(f22036,plain,
! [X0,X1] :
( r2_hidden(sK390(X0,sK54,sK56,X1),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,X1) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,X1),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(forward_subsumption_resolution,[],[f22035,f11552]) ).
fof(f22040,plain,
! [X0] :
( ~ m1_subset_1(np__0,k1_zfmisc_1(sK54))
| a_4_1_waybel22(sK54,sK55,sK56,np__0) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,np__0),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) ),
inference(resolution,[],[f22036,f15334]) ).
fof(f22101,plain,
! [X0] : a_4_1_waybel22(sK54,sK55,sK56,np__0) = k4_xboole_0(a_4_1_waybel22(sK54,sK55,sK56,np__0),k3_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))),
inference(forward_subsumption_resolution,[],[f22040,f14495]) ).
fof(f24402,plain,
( v3_struct_0(sK55)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(resolution,[],[f21313,f11553]) ).
fof(f24408,plain,
( ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24402,f11551]) ).
fof(f24411,plain,
( ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24408,f11550]) ).
fof(f24412,plain,
( ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24411,f11549]) ).
fof(f24413,plain,
( ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24412,f11548]) ).
fof(f24414,plain,
( ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24413,f11547]) ).
fof(f24415,plain,
( ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24414,f11546]) ).
fof(f24416,plain,
( ~ v1_funct_1(sK56)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24415,f11545]) ).
fof(f24417,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| np__0 = u1_struct_0(sK55)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55)) ),
inference(forward_subsumption_resolution,[],[f24416,f11554]) ).
fof(f24418,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_16 ),
inference(forward_subsumption_resolution,[],[f24417,f15899]) ).
fof(f24419,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| spl481_16 ),
inference(forward_subsumption_resolution,[],[f24418,f11552]) ).
fof(f24435,definition,
( spl481_217
<=> m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55)) ),
introduced(definition,[new_symbols(definition,[spl481_217])],[avatar_definition]) ).
fof(f24436,plain,
( m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ spl481_217 ),
inference(avatar_component_clause,[],[f24435]) ).
fof(f24437,plain,
( ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| spl481_217 ),
inference(avatar_component_clause,[],[f24435]) ).
fof(f24439,definition,
( spl481_218
<=> v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55)) ),
introduced(definition,[new_symbols(definition,[spl481_218])],[avatar_definition]) ).
fof(f24440,plain,
( v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ spl481_218 ),
inference(avatar_component_clause,[],[f24439]) ).
fof(f24441,plain,
( ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| spl481_218 ),
inference(avatar_component_clause,[],[f24439]) ).
fof(f24443,definition,
( spl481_219
<=> v3_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))) ),
introduced(definition,[new_symbols(definition,[spl481_219])],[avatar_definition]) ).
fof(f24444,plain,
( ~ v3_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| spl481_219 ),
inference(avatar_component_clause,[],[f24443]) ).
fof(f24445,plain,
( v3_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| ~ spl481_219 ),
inference(avatar_component_clause,[],[f24443]) ).
fof(f24450,plain,
( ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(resolution,[],[f24437,f15717]) ).
fof(f24451,plain,
( ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24450,f11550]) ).
fof(f24452,plain,
( ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24451,f11549]) ).
fof(f24453,plain,
( ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24452,f11548]) ).
fof(f24454,plain,
( ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24453,f11547]) ).
fof(f24455,plain,
( ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24454,f11546]) ).
fof(f24456,plain,
( ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24455,f11545]) ).
fof(f24457,plain,
( ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24456,f11554]) ).
fof(f24458,plain,
( ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24457,f11553]) ).
fof(f24459,plain,
( v3_struct_0(sK55)
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24458,f15699]) ).
fof(f24460,plain,
( $false
| spl481_217 ),
inference(forward_subsumption_resolution,[],[f24459,f11551]) ).
fof(f24461,plain,
spl481_217,
inference(avatar_contradiction_clause,[],[f24460]) ).
fof(f24462,plain,
( v3_struct_0(sK55)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(resolution,[],[f24441,f14448]) ).
fof(f24465,plain,
( ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24462,f11551]) ).
fof(f24467,plain,
( ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24465,f11550]) ).
fof(f24469,plain,
( ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24467,f11549]) ).
fof(f24471,plain,
( ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24469,f11548]) ).
fof(f24473,plain,
( ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24471,f11547]) ).
fof(f24475,plain,
( ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24473,f11546]) ).
fof(f24477,plain,
( ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24475,f11545]) ).
fof(f24479,plain,
( ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24477,f11554]) ).
fof(f24481,plain,
( ~ m1_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24479,f11553]) ).
fof(f24483,plain,
( $false
| spl481_218 ),
inference(forward_subsumption_resolution,[],[f24481,f15699]) ).
fof(f24484,plain,
spl481_218,
inference(avatar_contradiction_clause,[],[f24483]) ).
fof(f24495,plain,
( ! [X0] :
( v3_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| ~ l1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0)
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_218 ),
inference(resolution,[],[f24440,f11574]) ).
fof(f24543,plain,
( v1_xboole_0(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))
| ~ spl481_219 ),
inference(resolution,[],[f24445,f11987]) ).
fof(f24565,plain,
( v3_struct_0(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v2_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v2_yellow_0(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ spl481_219 ),
inference(resolution,[],[f24543,f11617]) ).
fof(f24566,plain,
( ~ v2_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v2_yellow_0(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ spl481_219 ),
inference(forward_subsumption_resolution,[],[f24565,f14505]) ).
fof(f24567,plain,
( ~ v3_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v2_yellow_0(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ spl481_219 ),
inference(forward_subsumption_resolution,[],[f24566,f14507]) ).
fof(f24568,plain,
( ~ v4_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ v2_yellow_0(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ spl481_219 ),
inference(forward_subsumption_resolution,[],[f24567,f14508]) ).
fof(f24569,plain,
( ~ v2_yellow_0(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ spl481_219 ),
inference(forward_subsumption_resolution,[],[f24568,f14509]) ).
fof(f24570,plain,
( ~ l1_orders_2(k2_yellow_1(k1_zfmisc_1(sK54)))
| ~ spl481_219 ),
inference(forward_subsumption_resolution,[],[f24569,f14511]) ).
fof(f24571,plain,
( $false
| ~ spl481_219 ),
inference(forward_subsumption_resolution,[],[f24570,f11981]) ).
fof(f24572,plain,
~ spl481_219,
inference(avatar_contradiction_clause,[],[f24571]) ).
fof(f24583,plain,
( ! [X0] :
( ~ l1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0)
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24495,f24444]) ).
fof(f24597,plain,
( ! [X0] :
( v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0)
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24583,f16016]) ).
fof(f24611,plain,
( ! [X0] :
( ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0)
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24597,f11551]) ).
fof(f24625,plain,
( ! [X0] :
( ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0)
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24611,f15723]) ).
fof(f24639,plain,
( ! [X0] :
( k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0)
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24625,f15712]) ).
fof(f24652,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| k1_funct_1(k2_waybel22(sK54,sK55,sK56),X0) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),X0) )
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24639,f24436]) ).
fof(f24676,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) = k1_funct_1(k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(resolution,[],[f24652,f11569]) ).
fof(f24685,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) = k1_funct_1(k2_waybel22(sK54,sK55,sK56),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24676,f11981]) ).
fof(f24692,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))),sK55,k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)) = k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_demodulation,[],[f24685,f14407]) ).
fof(f24698,plain,
( k1_yellow_0(sK55,a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54))) = k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54))
| spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(superposition,[],[f24419,f24692]) ).
fof(f24699,plain,
( k4_yellow_0(sK55) != k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(superposition,[],[f15755,f24692]) ).
fof(f24700,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| v3_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| ~ l1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(superposition,[],[f11575,f24692]) ).
fof(f24712,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ l1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24700,f24444]) ).
fof(f24718,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| v3_struct_0(sK55)
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24712,f16016]) ).
fof(f24724,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ l1_struct_0(sK55)
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24718,f11551]) ).
fof(f24730,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ v1_funct_1(k2_waybel22(sK54,sK55,sK56))
| ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24724,f15723]) ).
fof(f24736,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ v1_funct_2(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24730,f15712]) ).
fof(f24742,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ m1_relset_1(k2_waybel22(sK54,sK55,sK56),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24736,f24440]) ).
fof(f24748,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ m1_subset_1(k1_zfmisc_1(sK54),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24742,f24436]) ).
fof(f24754,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(forward_subsumption_resolution,[],[f24748,f15758]) ).
fof(f24757,definition,
( spl481_221
<=> m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55)) ),
introduced(definition,[new_symbols(definition,[spl481_221])],[avatar_definition]) ).
fof(f24758,plain,
( m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ spl481_221 ),
inference(avatar_component_clause,[],[f24757]) ).
fof(f24765,plain,
( spl481_221
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(avatar_split_clause,[],[f24754,f24443,f24439,f24435,f24757]) ).
fof(f24767,plain,
( ~ m1_subset_1(k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54)),u1_struct_0(sK55))
| ~ r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| k4_yellow_0(sK55) = k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54))
| spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219 ),
inference(superposition,[],[f19778,f24698]) ).
fof(f24788,plain,
( ~ r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| k4_yellow_0(sK55) = k1_funct_1(k2_waybel22(sK54,sK55,sK56),k1_zfmisc_1(sK54))
| spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219
| ~ spl481_221 ),
inference(forward_subsumption_resolution,[],[f24767,f24758]) ).
fof(f24795,plain,
( ~ r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219
| ~ spl481_221 ),
inference(forward_subsumption_resolution,[],[f24788,f24699]) ).
fof(f27896,plain,
! [X0] : ~ r2_hidden(X0,a_4_1_waybel22(sK54,sK55,sK56,np__0)),
inference(superposition,[],[f15468,f22101]) ).
fof(f27920,definition,
( spl481_318
<=> np__0 = a_4_1_waybel22(sK54,sK55,sK56,np__0) ),
introduced(definition,[new_symbols(definition,[spl481_318])],[avatar_definition]) ).
fof(f27922,plain,
( np__0 = a_4_1_waybel22(sK54,sK55,sK56,np__0)
| ~ spl481_318 ),
inference(avatar_component_clause,[],[f27920]) ).
fof(f28373,plain,
np__0 = a_4_1_waybel22(sK54,sK55,sK56,np__0),
inference(resolution,[],[f14722,f27896]) ).
fof(f28384,plain,
spl481_318,
inference(avatar_split_clause,[],[f28373,f27920]) ).
fof(f28633,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ m1_subset_1(np__0,k1_zfmisc_1(sK54))
| ~ r2_hidden(np__0,X0)
| v3_struct_0(sK55)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(superposition,[],[f15373,f27922]) ).
fof(f28634,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| v3_struct_0(sK55)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28633,f14495]) ).
fof(f28636,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v2_orders_2(sK55)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28634,f11551]) ).
fof(f28637,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v3_orders_2(sK55)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28636,f11550]) ).
fof(f28638,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v4_orders_2(sK55)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28637,f11549]) ).
fof(f28639,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v3_lattice3(sK55)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28638,f11548]) ).
fof(f28640,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v3_waybel_3(sK55)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28639,f11547]) ).
fof(f28641,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ l1_orders_2(sK55)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28640,f11546]) ).
fof(f28642,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v1_funct_1(sK56)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28641,f11545]) ).
fof(f28643,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ v1_funct_2(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28642,f11554]) ).
fof(f28644,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ m2_relset_1(sK56,k1_waybel22(sK54),u1_struct_0(sK55))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28643,f11553]) ).
fof(f28645,plain,
( ! [X0] :
( r2_hidden(k2_yellow_0(sK55,np__0),a_4_0_waybel22(sK54,sK55,sK56,X0))
| ~ r2_hidden(np__0,X0)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))) )
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28644,f11552]) ).
fof(f28646,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| ~ r2_hidden(np__0,X0)
| r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,X0)) )
| ~ spl481_318 ),
inference(forward_demodulation,[],[f28645,f15702]) ).
fof(f28650,plain,
( ~ r2_hidden(np__0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))))
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))
| ~ spl481_318 ),
inference(resolution,[],[f28646,f11569]) ).
fof(f28660,plain,
( ~ r2_hidden(np__0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54))))))
| r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))))
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28650,f11981]) ).
fof(f28668,plain,
( ~ r2_hidden(np__0,k1_zfmisc_1(sK54))
| r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))))
| ~ spl481_318 ),
inference(forward_demodulation,[],[f28660,f14407]) ).
fof(f28670,plain,
( r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK54)))))))
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28668,f16632]) ).
fof(f28672,plain,
( r2_hidden(k4_yellow_0(sK55),a_4_0_waybel22(sK54,sK55,sK56,k1_zfmisc_1(sK54)))
| ~ spl481_318 ),
inference(forward_demodulation,[],[f28670,f14407]) ).
fof(f28682,plain,
( $false
| spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219
| ~ spl481_221
| ~ spl481_318 ),
inference(forward_subsumption_resolution,[],[f28672,f24795]) ).
fof(f28683,plain,
( spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219
| ~ spl481_221
| ~ spl481_318 ),
inference(avatar_contradiction_clause,[],[f28682]) ).
cnf(s19,plain,
~ spl481_16,
inference(sat_conversion,[],[f15970]) ).
cnf(s199,plain,
spl481_217,
inference(sat_conversion,[],[f24461]) ).
cnf(s200,plain,
spl481_218,
inference(sat_conversion,[],[f24484]) ).
cnf(s202,plain,
~ spl481_219,
inference(sat_conversion,[],[f24572]) ).
cnf(s204,plain,
( ~ spl481_217
| ~ spl481_218
| spl481_219
| spl481_221 ),
inference(sat_conversion,[],[f24765]) ).
cnf(s333,plain,
spl481_318,
inference(sat_conversion,[],[f28384]) ).
cnf(s356,plain,
( spl481_16
| ~ spl481_217
| ~ spl481_218
| spl481_219
| ~ spl481_221
| ~ spl481_318 ),
inference(sat_conversion,[],[f28683]) ).
cnf(s380,plain,
spl481_221,
inference(rat,[],[s204,s200,s202,s199]) ).
cnf(s382,plain,
spl481_16,
inference(rat,[],[s356,s333,s199,s202,s200,s380]) ).
cnf(s446,plain,
$false,
inference(rat,[],[s19,s382]) ).
fof(f28684,plain,
$false,
inference(avatar_sat_refutation,[],[s446]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT350+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:54:31 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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.12/3.50 % (2119221)Detected formulas, will run a generic FOF schedule.
% 16.12/3.50 % (2119227)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=1901079768:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2995 on theBenchmark for (2995ds/134677Mi)
% 16.12/3.50 % (2119226)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=3868150849:i=141193_2995 on theBenchmark for (2995ds/141193Mi)
% 16.12/3.50 % (2119228)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=1853544702:i=141695:sd=1:nm=32:gsp=on:ss=included_2995 on theBenchmark for (2995ds/141695Mi)
% 16.12/3.50 % (2119230)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1598558305:i=119:av=off:ss=axioms_2995 on theBenchmark for (2995ds/119Mi)
% 16.12/3.50 % (2119231)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=684759560:s2a=on:i=139:gtg=position_2995 on theBenchmark for (2995ds/139Mi)
% 16.12/3.50 % (2119229)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=96072232:i=109:sd=1:ins=1:gsp=on:ss=axioms_2995 on theBenchmark for (2995ds/109Mi)
% 16.12/3.50 % (2119232)dis-21_1_sil=8000:lcm=predicate:random_seed=3751614044:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2995 on theBenchmark for (2995ds/129Mi)
% 16.12/3.50 % (2119229)Refutation not found, incomplete strategy
% 16.12/3.50 % (2119229)------------------------------
% 16.12/3.50 % (2119229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.12/3.50 % (2119229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/3.50 % (2119229)CaDiCaL version: 2.1.3
% 16.12/3.50 % (2119229)Termination reason: Refutation not found, incomplete strategy
% 16.12/3.50 % (2119229)Time elapsed: 0.046 s
% 16.12/3.50 % (2119229)Peak memory usage: 100 MB
% 16.12/3.50 % (2119229)Instructions burned: 56 (million)
% 16.12/3.50 % (2119231)Instruction limit reached!
% 16.12/3.50 % (2119231)------------------------------
% 16.12/3.50 % (2119231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.12/3.50 % (2119231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/3.50 % (2119231)CaDiCaL version: 2.1.3
% 16.12/3.50 % (2119231)Termination reason: Instruction limit
% 16.12/3.50 % (2119231)Termination phase: SInE selection
% 16.12/3.50 % (2119231)Time elapsed: 0.070 s
% 16.12/3.50 % (2119231)Peak memory usage: 96 MB
% 16.12/3.50 % (2119231)Instructions burned: 139 (million)
% 16.12/3.50 % (2119230)Instruction limit reached!
% 16.12/3.50 % (2119230)------------------------------
% 16.12/3.50 % (2119230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.12/3.50 % (2119230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/3.50 % (2119230)CaDiCaL version: 2.1.3
% 16.12/3.50 % (2119230)Termination reason: Instruction limit
% 16.12/3.50 % (2119230)Termination phase: Function definition elimination
% 16.12/3.50 % (2119230)Time elapsed: 0.086 s
% 16.12/3.50 % (2119230)Peak memory usage: 100 MB
% 16.12/3.50 % (2119230)Instructions burned: 120 (million)
% 16.12/3.50 % (2119232)Instruction limit reached!
% 16.12/3.50 % (2119232)------------------------------
% 16.12/3.50 % (2119232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.12/3.50 % (2119232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.12/3.50 % (2119232)CaDiCaL version: 2.1.3
% 16.12/3.50 % (2119232)Termination reason: Instruction limit
% 16.12/3.50 % (2119232)Termination phase: Unused predicate definition removal
% 16.12/3.50 % (2119232)Time elapsed: 0.103 s
% 16.12/3.50 % (2119232)Peak memory usage: 97 MB
% 16.12/3.50 % (2119232)Instructions burned: 129 (million)
% 16.12/3.50 % (2119240)lrs+10_1_sil=8000:sp=occurrence:random_seed=2980243745:i=285:sd=3:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/285Mi)
% 16.12/3.50 % (2119241)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4181616257:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2993 on theBenchmark for (2993ds/157Mi)
% 16.12/3.50 % (2119242)lrs+1011_1_sil=32000:sp=occurrence:random_seed=925730931:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 16.12/3.50 % (2119229)------------------------------
% 16.12/3.50 % (2119229)------------------------------
% 16.12/3.50 % (2119241)Instruction limit reached!
% 16.12/3.50 % (2119241)------------------------------
% 16.12/3.50 % (2119241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.58 % (2119241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.58 % (2119241)CaDiCaL version: 2.1.3
% 23.22/4.58 % (2119241)Termination reason: Instruction limit
% 23.22/4.58 % (2119241)Termination phase: Preprocessing 3
% 23.22/4.58 % (2119241)Time elapsed: 0.085 s
% 23.22/4.58 % (2119241)Peak memory usage: 97 MB
% 23.22/4.58 % (2119241)Instructions burned: 157 (million)
% 23.22/4.58 % (2119242)Refutation not found, incomplete strategy
% 23.22/4.58 % (2119242)------------------------------
% 23.22/4.58 % (2119242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.58 % (2119242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.58 % (2119242)CaDiCaL version: 2.1.3
% 23.22/4.58 % (2119242)Termination reason: Refutation not found, incomplete strategy
% 23.22/4.58 % (2119242)Time elapsed: 0.057 s
% 23.22/4.58 % (2119242)Peak memory usage: 101 MB
% 23.22/4.58 % (2119242)Instructions burned: 72 (million)
% 23.22/4.58 % (2119240)Instruction limit reached!
% 23.22/4.58 % (2119240)------------------------------
% 23.22/4.58 % (2119240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.58 % (2119240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.58 % (2119240)CaDiCaL version: 2.1.3
% 23.22/4.58 % (2119240)Termination reason: Instruction limit
% 23.22/4.58 % (2119240)Termination phase: Saturation
% 23.22/4.58 % (2119240)Time elapsed: 0.187 s
% 23.22/4.58 % (2119240)Peak memory usage: 104 MB
% 23.22/4.58 % (2119240)Instructions burned: 285 (million)
% 23.22/4.58 % (2119246)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=766330918:s2a=on:i=248:s2at=1.23:gtg=position_2991 on theBenchmark for (2991ds/248Mi)
% 23.22/4.58 % (2119247)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1094807709:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 23.22/4.58 % (2119242)------------------------------
% 23.22/4.58 % (2119242)------------------------------
% 23.22/4.58 % (2119248)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3612098875:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 23.22/4.58 % (2119246)Instruction limit reached!
% 23.22/4.58 % (2119246)------------------------------
% 23.22/4.58 % (2119246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.58 % (2119246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.58 % (2119246)CaDiCaL version: 2.1.3
% 23.22/4.58 % (2119246)Termination reason: Instruction limit
% 23.22/4.58 % (2119246)Termination phase: Unused predicate definition removal
% 23.22/4.58 % (2119246)Time elapsed: 0.148 s
% 23.22/4.58 % (2119246)Peak memory usage: 99 MB
% 23.22/4.58 % (2119246)Instructions burned: 248 (million)
% 23.22/4.58 % (2119247)Instruction limit reached!
% 23.22/4.58 % (2119247)------------------------------
% 23.22/4.58 % (2119247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.58 % (2119247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.58 % (2119247)CaDiCaL version: 2.1.3
% 23.22/4.58 % (2119247)Termination reason: Instruction limit
% 23.22/4.58 % (2119247)Termination phase: Saturation
% 23.22/4.58 % (2119247)Time elapsed: 0.175 s
% 23.22/4.58 % (2119247)Peak memory usage: 104 MB
% 23.22/4.58 % (2119247)Instructions burned: 294 (million)
% 23.22/4.58 % (2119252)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3613464050:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 23.22/4.58 % (2119253)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1973020158:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 23.22/4.58 % (2119254)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=656218234:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 23.22/4.58 % (2119252)Instruction limit reached!
% 23.22/4.58 % (2119252)------------------------------
% 23.22/4.58 % (2119252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.22/4.58 % (2119252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.22/4.58 % (2119252)CaDiCaL version: 2.1.3
% 23.22/4.58 % (2119252)Termination reason: Instruction limit
% 23.22/4.58 % (2119252)Termination phase: Property scanning
% 23.22/4.58 % (2119252)Time elapsed: 0.088 s
% 23.22/4.58 % (2119252)Peak memory usage: 100 MB
% 51.26/8.46 % (2119252)Instructions burned: 114 (million)
% 51.26/8.46 % (2119253)Instruction limit reached!
% 51.26/8.46 % (2119253)------------------------------
% 51.26/8.46 % (2119253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.26/8.46 % (2119253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.26/8.46 % (2119253)CaDiCaL version: 2.1.3
% 51.26/8.46 % (2119253)Termination reason: Instruction limit
% 51.26/8.46 % (2119253)Termination phase: Naming
% 51.26/8.46 % (2119253)Time elapsed: 0.099 s
% 51.26/8.46 % (2119253)Peak memory usage: 105 MB
% 51.26/8.46 % (2119253)Instructions burned: 128 (million)
% 51.26/8.46 % (2119254)Instruction limit reached!
% 51.26/8.46 % (2119254)------------------------------
% 51.26/8.46 % (2119254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.26/8.46 % (2119254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.26/8.46 % (2119254)CaDiCaL version: 2.1.3
% 51.26/8.46 % (2119254)Termination reason: Instruction limit
% 51.26/8.46 % (2119254)Termination phase: Initialization
% 51.26/8.46 % (2119254)Time elapsed: 0.051 s
% 51.26/8.46 % (2119254)Peak memory usage: 96 MB
% 51.26/8.46 % (2119254)Instructions burned: 116 (million)
% 51.26/8.46 % (2119258)lrs+10_1_sil=8000:sp=occurrence:random_seed=1169949636:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 51.26/8.46 % (2119259)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2370460065:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 51.26/8.46 % (2119260)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3550071959:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 51.26/8.46 % (2119259)Refutation not found, incomplete strategy
% 51.26/8.46 % (2119259)------------------------------
% 51.26/8.46 % (2119259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.26/8.46 % (2119259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.26/8.46 % (2119259)CaDiCaL version: 2.1.3
% 51.26/8.46 % (2119259)Termination reason: Refutation not found, incomplete strategy
% 51.26/8.46 % (2119259)Time elapsed: 0.072 s
% 51.26/8.46 % (2119259)Peak memory usage: 101 MB
% 51.26/8.46 % (2119259)Instructions burned: 104 (million)
% 51.26/8.47 % (2119259)------------------------------
% 51.26/8.47 % (2119259)------------------------------
% 51.26/8.47 % (2119264)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3880084260:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 51.26/8.47 % (2119258)Instruction limit reached!
% 51.26/8.47 % (2119258)------------------------------
% 51.26/8.47 % (2119258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.26/8.47 % (2119258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.26/8.47 % (2119258)CaDiCaL version: 2.1.3
% 51.26/8.47 % (2119258)Termination reason: Instruction limit
% 51.26/8.47 % (2119258)Termination phase: Saturation
% 51.26/8.47 % (2119258)Time elapsed: 0.524 s
% 51.26/8.47 % (2119258)Peak memory usage: 114 MB
% 51.26/8.47 % (2119258)Instructions burned: 907 (million)
% 51.26/8.47 % (2119264)Instruction limit reached!
% 51.26/8.47 % (2119264)------------------------------
% 51.26/8.47 % (2119264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.26/8.47 % (2119264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.26/8.47 % (2119264)CaDiCaL version: 2.1.3
% 51.26/8.47 % (2119264)Termination reason: Instruction limit
% 51.26/8.47 % (2119264)Termination phase: Property scanning
% 51.26/8.47 % (2119264)Time elapsed: 0.091 s
% 51.26/8.47 % (2119264)Peak memory usage: 100 MB
% 51.26/8.47 % (2119264)Instructions burned: 137 (million)
% 51.26/8.47 % (2119266)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2523973743:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 51.26/8.47 % (2119267)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2636032308:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 51.26/8.47 % (2119266)Instruction limit reached!
% 51.26/8.47 % (2119266)------------------------------
% 51.26/8.47 % (2119266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.26/8.47 % (2119266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.26/8.47 % (2119266)CaDiCaL version: 2.1.3
% 51.26/8.47 % (2119266)Termination reason: Instruction limit
% 51.26/8.47 % (2119266)Termination phase: Property scanning
% 84.20/13.08 % (2119266)Time elapsed: 0.368 s
% 84.20/13.08 % (2119266)Peak memory usage: 113 MB
% 84.20/13.08 % (2119266)Instructions burned: 595 (million)
% 84.20/13.08 % (2119248)Instruction limit reached!
% 84.20/13.08 % (2119248)------------------------------
% 84.20/13.08 % (2119248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.20/13.08 % (2119248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.20/13.08 % (2119248)CaDiCaL version: 2.1.3
% 84.20/13.08 % (2119248)Termination reason: Instruction limit
% 84.20/13.08 % (2119248)Termination phase: Saturation
% 84.20/13.08 % (2119248)Time elapsed: 1.582 s
% 84.20/13.08 % (2119248)Peak memory usage: 313 MB
% 84.20/13.08 % (2119248)Instructions burned: 2352 (million)
% 84.20/13.08 % (2119270)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=420231656:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 84.20/13.08 % (2119270)Instruction limit reached!
% 84.20/13.08 % (2119270)------------------------------
% 84.20/13.08 % (2119270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.20/13.08 % (2119270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.20/13.08 % (2119270)CaDiCaL version: 2.1.3
% 84.20/13.08 % (2119270)Termination reason: Instruction limit
% 84.20/13.08 % (2119270)Termination phase: SInE selection
% 84.20/13.08 % (2119270)Time elapsed: 0.060 s
% 84.20/13.08 % (2119270)Peak memory usage: 96 MB
% 84.20/13.08 % (2119270)Instructions burned: 125 (million)
% 84.20/13.08 % (2119271)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2624812284:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 84.20/13.08 % (2119271)Instruction limit reached!
% 84.20/13.08 % (2119271)------------------------------
% 84.20/13.08 % (2119271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.20/13.08 % (2119271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.20/13.08 % (2119271)CaDiCaL version: 2.1.3
% 84.20/13.08 % (2119271)Termination reason: Instruction limit
% 84.20/13.08 % (2119271)Termination phase: Initialization
% 84.20/13.08 % (2119271)Time elapsed: 0.063 s
% 84.20/13.08 % (2119271)Peak memory usage: 96 MB
% 84.20/13.08 % (2119271)Instructions burned: 136 (million)
% 84.20/13.08 % (2119273)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1289475266:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 84.20/13.08 % (2119273)Refutation not found, incomplete strategy
% 84.20/13.08 % (2119273)------------------------------
% 84.20/13.08 % (2119273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.20/13.08 % (2119273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.20/13.08 % (2119273)CaDiCaL version: 2.1.3
% 84.20/13.08 % (2119273)Termination reason: Refutation not found, incomplete strategy
% 84.20/13.08 % (2119273)Time elapsed: 0.047 s
% 84.20/13.08 % (2119273)Peak memory usage: 100 MB
% 84.20/13.08 % (2119273)Instructions burned: 53 (million)
% 84.20/13.08 % (2119275)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=546966291:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2969 on theBenchmark for (2969ds/431Mi)
% 84.20/13.08 % (2119273)------------------------------
% 84.20/13.08 % (2119273)------------------------------
% 84.20/13.08 % (2119275)Instruction limit reached!
% 84.20/13.08 % (2119275)------------------------------
% 84.20/13.08 % (2119275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.20/13.08 % (2119275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.20/13.08 % (2119275)CaDiCaL version: 2.1.3
% 84.20/13.08 % (2119275)Termination reason: Instruction limit
% 84.20/13.08 % (2119275)Termination phase: Saturation
% 84.20/13.08 % (2119275)Time elapsed: 0.254 s
% 84.20/13.08 % (2119275)Peak memory usage: 102 MB
% 84.20/13.08 % (2119275)Instructions burned: 431 (million)
% 84.20/13.08 % (2119278)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=386992765:i=6060:aac=none:ins=25_2966 on theBenchmark for (2966ds/6060Mi)
% 84.20/13.08 % (2119279)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=373067448:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 84.20/13.08 % (2119279)Instruction limit reached!
% 48.23/15.31 % (2119279)------------------------------
% 48.23/15.31 % (2119279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119279)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119279)Termination reason: Instruction limit
% 48.23/15.31 % (2119279)Termination phase: Preprocessing 2
% 48.23/15.31 % (2119279)Time elapsed: 0.117 s
% 48.23/15.31 % (2119279)Peak memory usage: 104 MB
% 48.23/15.31 % (2119279)Instructions burned: 151 (million)
% 48.23/15.31 % (2119282)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2956676363:i=14155:bd=all_2962 on theBenchmark for (2962ds/14155Mi)
% 48.23/15.31 % (2119260)Instruction limit reached!
% 48.23/15.31 % (2119260)------------------------------
% 48.23/15.31 % (2119260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119260)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119260)Termination reason: Instruction limit
% 48.23/15.31 % (2119260)Termination phase: Saturation
% 48.23/15.31 % (2119260)Time elapsed: 3.224 s
% 48.23/15.31 % (2119260)Peak memory usage: 180 MB
% 48.23/15.31 % (2119260)Instructions burned: 5203 (million)
% 48.23/15.31 % (2119284)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2488952769:i=667:av=off:fsr=off_2951 on theBenchmark for (2951ds/667Mi)
% 48.23/15.31 % (2119284)Instruction limit reached!
% 48.23/15.31 % (2119284)------------------------------
% 48.23/15.31 % (2119284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119284)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119284)Termination reason: Instruction limit
% 48.23/15.31 % (2119284)Termination phase: Property scanning
% 48.23/15.31 % (2119284)Time elapsed: 0.424 s
% 48.23/15.31 % (2119284)Peak memory usage: 120 MB
% 48.23/15.31 % (2119284)Instructions burned: 668 (million)
% 48.23/15.31 % (2119286)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=2484926939:s2a=on:i=185:s2at=1.8:fdi=4_2945 on theBenchmark for (2945ds/185Mi)
% 48.23/15.31 % (2119286)Instruction limit reached!
% 48.23/15.31 % (2119286)------------------------------
% 48.23/15.31 % (2119286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119286)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119286)Termination reason: Instruction limit
% 48.23/15.31 % (2119286)Termination phase: NewCNF
% 48.23/15.31 % (2119286)Time elapsed: 0.147 s
% 48.23/15.31 % (2119286)Peak memory usage: 105 MB
% 48.23/15.31 % (2119286)Instructions burned: 185 (million)
% 48.23/15.31 % (2119288)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3128295287:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2942 on theBenchmark for (2942ds/193Mi)
% 48.23/15.31 % (2119288)Instruction limit reached!
% 48.23/15.31 % (2119288)------------------------------
% 48.23/15.31 % (2119288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119288)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119288)Termination reason: Instruction limit
% 48.23/15.31 % (2119288)Termination phase: Property scanning
% 48.23/15.31 % (2119288)Time elapsed: 0.139 s
% 48.23/15.31 % (2119288)Peak memory usage: 100 MB
% 48.23/15.31 % (2119288)Instructions burned: 194 (million)
% 48.23/15.31 % (2119290)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1378428193:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2938 on theBenchmark for (2938ds/4850Mi)
% 48.23/15.31 % (2119278)Instruction limit reached!
% 48.23/15.31 % (2119278)------------------------------
% 48.23/15.31 % (2119278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119278)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119278)Termination reason: Instruction limit
% 48.23/15.31 % (2119278)Termination phase: Saturation
% 48.23/15.31 % (2119278)Time elapsed: 3.871 s
% 48.23/15.31 % (2119278)Peak memory usage: 336 MB
% 48.23/15.31 % (2119278)Instructions burned: 6061 (million)
% 48.23/15.31 % (2119292)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1673885206:i=12111:sd=1:ss=included_2925 on theBenchmark for (2925ds/12111Mi)
% 48.23/15.31 % (2119290)Instruction limit reached!
% 48.23/15.31 % (2119290)------------------------------
% 48.23/15.31 % (2119290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119290)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119290)Termination reason: Instruction limit
% 48.23/15.31 % (2119290)Termination phase: Saturation
% 48.23/15.31 % (2119290)Time elapsed: 2.483 s
% 48.23/15.31 % (2119290)Peak memory usage: 144 MB
% 48.23/15.31 % (2119290)Instructions burned: 4850 (million)
% 48.23/15.31 % (2119294)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3660176825:i=319:kws=precedence:fsr=off_2912 on theBenchmark for (2912ds/319Mi)
% 48.23/15.31 % (2119294)Instruction limit reached!
% 48.23/15.31 % (2119294)------------------------------
% 48.23/15.31 % (2119294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119294)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119294)Termination reason: Instruction limit
% 48.23/15.31 % (2119294)Termination phase: Preprocessing 3
% 48.23/15.31 % (2119294)Time elapsed: 0.209 s
% 48.23/15.31 % (2119294)Peak memory usage: 113 MB
% 48.23/15.31 % (2119294)Instructions burned: 319 (million)
% 48.23/15.31 % (2119296)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1185205958:i=2064:ep=RST_2908 on theBenchmark for (2908ds/2064Mi)
% 48.23/15.31 % (2119267)Instruction limit reached!
% 48.23/15.31 % (2119267)------------------------------
% 48.23/15.31 % (2119267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119267)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119267)Termination reason: Instruction limit
% 48.23/15.31 % (2119267)Termination phase: Saturation
% 48.23/15.31 % (2119267)Time elapsed: 7.764 s
% 48.23/15.31 % (2119267)Peak memory usage: 244 MB
% 48.23/15.31 % (2119267)Instructions burned: 13194 (million)
% 48.23/15.31 % (2119296)Instruction limit reached!
% 48.23/15.31 % (2119296)------------------------------
% 48.23/15.31 % (2119296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119296)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119296)Termination reason: Instruction limit
% 48.23/15.31 % (2119296)Termination phase: Saturation
% 48.23/15.31 % (2119296)Time elapsed: 1.017 s
% 48.23/15.31 % (2119296)Peak memory usage: 150 MB
% 48.23/15.31 % (2119296)Instructions burned: 2065 (million)
% 48.23/15.31 % (2119298)dis-1011_128_sil=32000:random_seed=3314677087:i=3706:ep=RST:av=off_2898 on theBenchmark for (2898ds/3706Mi)
% 48.23/15.31 % (2119300)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2013944617:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2896 on theBenchmark for (2896ds/757Mi)
% 48.23/15.31 % (2119300)Instruction limit reached!
% 48.23/15.31 % (2119300)------------------------------
% 48.23/15.31 % (2119300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119300)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119300)Termination reason: Instruction limit
% 48.23/15.31 % (2119300)Termination phase: Saturation
% 48.23/15.31 % (2119300)Time elapsed: 0.499 s
% 48.23/15.31 % (2119300)Peak memory usage: 114 MB
% 48.23/15.31 % (2119300)Instructions burned: 757 (million)
% 48.23/15.31 % (2119302)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4244320624:i=13913:ss=axioms:sgt=8_2890 on theBenchmark for (2890ds/13913Mi)
% 48.23/15.31 % (2119282)Instruction limit reached!
% 48.23/15.31 % (2119282)------------------------------
% 48.23/15.31 % (2119282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119282)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119282)Termination reason: Instruction limit
% 48.23/15.31 % (2119282)Termination phase: Saturation
% 48.23/15.31 % (2119282)Time elapsed: 8.160 s
% 48.23/15.31 % (2119282)Peak memory usage: 411 MB
% 48.23/15.31 % (2119282)Instructions burned: 14156 (million)
% 48.23/15.31 % (2119298)Instruction limit reached!
% 48.23/15.31 % (2119298)------------------------------
% 48.23/15.31 % (2119298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119298)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119298)Termination reason: Instruction limit
% 48.23/15.31 % (2119298)Termination phase: Saturation
% 48.23/15.31 % (2119298)Time elapsed: 1.931 s
% 48.23/15.31 % (2119298)Peak memory usage: 146 MB
% 48.23/15.31 % (2119298)Instructions burned: 3706 (million)
% 48.23/15.31 % (2119304)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3698525837:i=9925:aac=none_2878 on theBenchmark for (2878ds/9925Mi)
% 48.23/15.31 % (2119305)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1413859796:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2877 on theBenchmark for (2877ds/2479Mi)
% 48.23/15.31 % (2119305)Instruction limit reached!
% 48.23/15.31 % (2119305)------------------------------
% 48.23/15.31 % (2119305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119305)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119305)Termination reason: Instruction limit
% 48.23/15.31 % (2119305)Termination phase: Saturation
% 48.23/15.31 % (2119305)Time elapsed: 1.492 s
% 48.23/15.31 % (2119305)Peak memory usage: 120 MB
% 48.23/15.31 % (2119305)Instructions burned: 2479 (million)
% 48.23/15.31 % (2119308)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1155981947:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2860 on theBenchmark for (2860ds/440Mi)
% 48.23/15.31 % (2119302)First to succeed.
% 48.23/15.31 % (2119302)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2119221"
% 48.23/15.31 % (2119308)Instruction limit reached!
% 48.23/15.31 % (2119308)------------------------------
% 48.23/15.31 % (2119308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.23/15.31 % (2119308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.23/15.31 % (2119308)CaDiCaL version: 2.1.3
% 48.23/15.31 % (2119308)Termination reason: Instruction limit
% 48.23/15.31 % (2119308)Termination phase: Naming
% 48.23/15.31 % (2119308)Time elapsed: 0.248 s
% 48.23/15.31 % (2119308)Peak memory usage: 109 MB
% 48.23/15.31 % (2119308)Instructions burned: 440 (million)
% 48.23/15.31 % (2119302)Refutation found. Thanks to Tanya!
% 48.23/15.31 % SZS status Theorem for theBenchmark
% 48.23/15.31 % SZS output start Proof for theBenchmark
% See solution above
% 100.45/15.55 % (2119302)------------------------------
% 100.45/15.55 % (2119302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.45/15.55 % (2119302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.45/15.55 % (2119302)CaDiCaL version: 2.1.3
% 100.45/15.55 % (2119302)Termination reason: Refutation
% 100.45/15.55 % (2119302)Time elapsed: 2.993 s
% 100.45/15.55 % (2119302)Peak memory usage: 180 MB
% 100.45/15.55 % (2119302)Instructions burned: 4630 (million)
% 100.45/15.55 % (2119302)------------------------------
% 100.45/15.55 % (2119302)------------------------------
% 100.45/15.55 % (2119221)Success in time 14.462 s
% 100.45/15.55 % Vampire exiting
%------------------------------------------------------------------------------