%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT350+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 64.87s 16.52s
% Output : Refutation 105.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 53
% Syntax : Number of formulae : 458 ( 60 unt; 12 def)
% Number of atoms : 2720 ( 240 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 3988 (1726 ~;1888 |; 274 &)
% ( 39 <=>; 61 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 8 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 41 ( 39 usr; 13 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 5 con; 0-5 aty)
% Number of variables : 572 ( 0 sgn 546 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f471,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f486,axiom,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset_1) ).
fof(f1394,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(f1638,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(f3551,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f7737,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(f7890,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(f11558,axiom,
! [X0] :
( ( v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0) )
=> ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_lattice3) ).
fof(f11559,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice3) ).
fof(f11589,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(f11637,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_lattice3) ).
fof(f14799,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( r1_yellow_0(X0,X1)
& r2_yellow_0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_yellow_0) ).
fof(f14829,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(f14831,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r1_orders_2(X0,X1,k4_yellow_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t45_yellow_0) ).
fof(f14869,axiom,
! [X0,X1] :
( l1_orders_2(X0)
=> m1_subset_1(k2_yellow_0(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_yellow_0) ).
fof(f14870,axiom,
! [X0] :
( l1_orders_2(X0)
=> m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_yellow_0) ).
fof(f14871,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(f14917,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( v2_orders_2(X0)
& v1_lattice3(X0)
& v24_waybel_0(X0) )
=> ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v1_lattice3(X0)
& v2_yellow_0(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc9_waybel_0) ).
fof(f14918,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_lattice3(X0) )
=> ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v24_waybel_0(X0)
& v25_waybel_0(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc10_waybel_0) ).
fof(f14954,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,k6_waybel_0(X0,X1))
<=> r1_orders_2(X0,X2,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_waybel_0) ).
fof(f14955,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_hidden(X2,k7_waybel_0(X0,X1))
<=> r1_orders_2(X0,X1,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_waybel_0) ).
fof(f14957,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(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))
=> ( k7_waybel_0(X0,X1) = k7_waybel_0(X0,X2)
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_waybel_0) ).
fof(f14978,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& v4_orders_2(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( r2_yellow_0(X0,k7_waybel_0(X0,X1))
& k2_yellow_0(X0,k7_waybel_0(X0,X1)) = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t39_waybel_0) ).
fof(f15095,axiom,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_yellow_1) ).
fof(f15126,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(f15166,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(f16049,axiom,
! [X0] :
( l1_orders_2(X0)
=> u1_struct_0(X0) = u1_struct_0(k7_lattice3(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_yellow_6) ).
fof(f16210,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v3_yellow_0(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_yellow_7) ).
fof(f16230,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( ( r1_yellow_0(X0,X1)
| r2_yellow_0(k7_lattice3(X0),X1) )
=> k1_yellow_0(X0,X1) = k2_yellow_0(k7_lattice3(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_yellow_7) ).
fof(f16235,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ( v3_lattice3(X0)
<=> v3_lattice3(k7_lattice3(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_yellow_7) ).
fof(f16238,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k7_lattice3(X0)))
=> ( X1 = X2
=> ( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
& k7_waybel_0(X0,X1) = k6_waybel_0(k7_lattice3(X0),X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t20_yellow_7) ).
fof(f16983,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v1_yellow_0(X0)
& l1_orders_2(X0) )
=> k7_waybel_0(X0,k3_yellow_0(X0)) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_waybel14) ).
fof(f16984,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v2_yellow_0(X0)
& l1_orders_2(X0) )
=> k6_waybel_0(X0,k4_yellow_0(X0)) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_waybel14) ).
fof(f17272,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(f17780,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(f17781,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(f17783,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(f17801,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(f17803,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(f17804,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)],[f17803]) ).
fof(f17871,plain,
? [X0,X1] :
( ? [X2] :
( k4_yellow_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)))))
& 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,[],[f17804]) ).
fof(f17872,plain,
? [X0,X1] :
( ? [X2] :
( k4_yellow_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)))))
& 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,[],[f17871]) ).
fof(f17875,plain,
! [X0] :
( ( v1_lattice3(X0)
& v2_lattice3(X0) )
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11589]) ).
fof(f17876,plain,
! [X0] :
( ( v1_lattice3(X0)
& v2_lattice3(X0) )
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f17875]) ).
fof(f17879,plain,
! [X0] :
( k6_waybel_0(X0,k4_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16984]) ).
fof(f17880,plain,
! [X0] :
( k6_waybel_0(X0,k4_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f17879]) ).
fof(f17895,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14871]) ).
fof(f17896,plain,
! [X0] :
( ! [X1] :
( r1_orders_2(X0,X1,k4_yellow_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14831]) ).
fof(f17897,plain,
! [X0] :
( ! [X1] :
( r1_orders_2(X0,X1,k4_yellow_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f17896]) ).
fof(f17898,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14829]) ).
fof(f17950,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,[],[f17801]) ).
fof(f17951,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,[],[f17950]) ).
fof(f17952,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,[],[f17783]) ).
fof(f17953,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,[],[f17952]) ).
fof(f17970,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,[],[f7737]) ).
fof(f17971,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,[],[f17970]) ).
fof(f17976,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v1_lattice3(X0)
& v2_yellow_0(X0) )
| ~ v2_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v24_waybel_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14917]) ).
fof(f17977,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v1_lattice3(X0)
& v2_yellow_0(X0) )
| ~ v2_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v24_waybel_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f17976]) ).
fof(f18008,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,k6_waybel_0(X0,X1))
<=> r1_orders_2(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14954]) ).
fof(f18009,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,k6_waybel_0(X0,X1))
<=> r1_orders_2(X0,X2,X1) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18008]) ).
fof(f18072,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f18096,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v3_yellow_0(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16210]) ).
fof(f18097,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0))
& v1_lattice3(k7_lattice3(X0))
& v2_lattice3(k7_lattice3(X0))
& v3_lattice3(k7_lattice3(X0))
& v1_yellow_0(k7_lattice3(X0))
& v2_yellow_0(k7_lattice3(X0))
& v3_yellow_0(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18096]) ).
fof(f18129,plain,
! [X0] :
( m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14870]) ).
fof(f18139,plain,
! [X0] :
( k7_waybel_0(X0,k3_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16983]) ).
fof(f18140,plain,
! [X0] :
( k7_waybel_0(X0,k3_yellow_0(X0)) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v1_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18139]) ).
fof(f18147,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
& k7_waybel_0(X0,X1) = k6_waybel_0(k7_lattice3(X0),X2) )
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16238]) ).
fof(f18148,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
& k7_waybel_0(X0,X1) = k6_waybel_0(k7_lattice3(X0),X2) )
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18147]) ).
fof(f18151,plain,
! [X0] :
( ! [X1] :
( ( r2_yellow_0(X0,k7_waybel_0(X0,X1))
& k2_yellow_0(X0,k7_waybel_0(X0,X1)) = X1 )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14978]) ).
fof(f18152,plain,
! [X0] :
( ! [X1] :
( ( r2_yellow_0(X0,k7_waybel_0(X0,X1))
& k2_yellow_0(X0,k7_waybel_0(X0,X1)) = X1 )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18151]) ).
fof(f18155,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| k7_waybel_0(X0,X1) != k7_waybel_0(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14957]) ).
fof(f18156,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| k7_waybel_0(X0,X1) != k7_waybel_0(X0,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18155]) ).
fof(f18157,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,k7_waybel_0(X0,X1))
<=> r1_orders_2(X0,X1,X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14955]) ).
fof(f18158,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r2_hidden(X2,k7_waybel_0(X0,X1))
<=> r1_orders_2(X0,X1,X2) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18157]) ).
fof(f18225,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,[],[f15166]) ).
fof(f18226,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,[],[f18225]) ).
fof(f18229,plain,
! [X0,X1] :
( m1_subset_1(k2_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14869]) ).
fof(f18381,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v24_waybel_0(X0)
& v25_waybel_0(X0) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14918]) ).
fof(f18382,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v24_waybel_0(X0)
& v25_waybel_0(X0) )
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18381]) ).
fof(f18500,plain,
! [X0] :
( ! [X1] :
( k1_yellow_0(X0,X1) = k2_yellow_0(k7_lattice3(X0),X1)
| ( ~ r1_yellow_0(X0,X1)
& ~ r2_yellow_0(k7_lattice3(X0),X1) ) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16230]) ).
fof(f18501,plain,
! [X0] :
( ! [X1] :
( k1_yellow_0(X0,X1) = k2_yellow_0(k7_lattice3(X0),X1)
| ( ~ r1_yellow_0(X0,X1)
& ~ r2_yellow_0(k7_lattice3(X0),X1) ) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18500]) ).
fof(f18542,plain,
! [X0] :
( ! [X1] :
( r1_yellow_0(X0,X1)
& r2_yellow_0(X0,X1) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f14799]) ).
fof(f18543,plain,
! [X0] :
( ! [X1] :
( r1_yellow_0(X0,X1)
& r2_yellow_0(X0,X1) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18542]) ).
fof(f18557,plain,
! [X0] :
( ( v3_lattice3(X0)
<=> v3_lattice3(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16235]) ).
fof(f18558,plain,
! [X0] :
( ( v3_lattice3(X0)
<=> v3_lattice3(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18557]) ).
fof(f18578,plain,
! [X0] :
( u1_struct_0(X0) = u1_struct_0(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16049]) ).
fof(f18579,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& l1_orders_2(k7_lattice3(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11637]) ).
fof(f18581,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11559]) ).
fof(f18582,plain,
! [X0] :
( ( ~ v3_struct_0(k7_lattice3(X0))
& v1_orders_2(k7_lattice3(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18581]) ).
fof(f18583,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f11558]) ).
fof(f18584,plain,
! [X0] :
( ( v1_orders_2(k7_lattice3(X0))
& v2_orders_2(k7_lattice3(X0))
& v3_orders_2(k7_lattice3(X0))
& v4_orders_2(k7_lattice3(X0)) )
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f18583]) ).
fof(f18790,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,[],[f7890]) ).
fof(f18791,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,[],[f18790]) ).
fof(f18808,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,[],[f17780]) ).
fof(f18809,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,[],[f18808]) ).
fof(f18947,plain,
! [X0] :
( k1_xboole_0 = X0
| ? [X1] :
( r2_hidden(X1,X0)
& ! [X2] :
( r1_xboole_0(X2,X0)
| ~ r2_hidden(X2,X1) ) ) ),
inference(ennf_transformation,[],[f1638]) ).
fof(f19669,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,[],[f17781]) ).
fof(f19670,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,[],[f19669]) ).
fof(f20055,plain,
( k4_yellow_0(sK68) != k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK67))),sK68,k2_waybel22(sK67,sK68,sK69),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK67)))))
& v1_funct_1(sK69)
& v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
& m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
& ~ v3_struct_0(sK68)
& v2_orders_2(sK68)
& v3_orders_2(sK68)
& v4_orders_2(sK68)
& v3_lattice3(sK68)
& v3_waybel_3(sK68)
& l1_orders_2(sK68) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67,sK68,sK69]),skolemize(X0,sK67),skolemize(X1,sK68),skolemize(X2,sK69)],[f17872]) ).
fof(f20078,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,[],[f17951]) ).
fof(f20079,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,[],[f20078]) ).
fof(f20080,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,sK85(X0,X1,X2,X3)) != k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,sK85(X0,X1,X2,X3)))
& m1_subset_1(sK85(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,[sK85]),skolemize(X4,sK85(X0,X1,X2,X3))],[f20079]) ).
fof(f20099,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X2,k6_waybel_0(X0,X1))
| ~ r1_orders_2(X0,X2,X1) )
& ( r1_orders_2(X0,X2,X1)
| ~ r2_hidden(X2,k6_waybel_0(X0,X1)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f18009]) ).
fof(f20117,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,[],[f18072]) ).
fof(f20143,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r2_hidden(X2,k7_waybel_0(X0,X1))
| ~ r1_orders_2(X0,X1,X2) )
& ( r1_orders_2(X0,X1,X2)
| ~ r2_hidden(X2,k7_waybel_0(X0,X1)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f18158]) ).
fof(f20167,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(f20168,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f20167]) ).
fof(f20169,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK140(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK140]),skolemize(X1,sK140(X0))],[f20168]) ).
fof(f20296,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,[],[f1394]) ).
fof(f20405,plain,
! [X0] :
( ( ( v3_lattice3(X0)
| ~ v3_lattice3(k7_lattice3(X0)) )
& ( v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(X0) ) )
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f18558]) ).
fof(f20480,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,[],[f18791]) ).
fof(f20497,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,[],[f18809]) ).
fof(f20498,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,[],[f20497]) ).
fof(f20499,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(sK290(X0,X1,X2,X3,X4),k1_zfmisc_1(X1))
& k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,sK290(X0,X1,X2,X3,X4))) = X0
& r2_hidden(sK290(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,[sK290]),skolemize(X6,sK290(X0,X1,X2,X3,X4))],[f20498]) ).
fof(f20563,plain,
! [X0] :
( k1_xboole_0 = X0
| ( r2_hidden(sK320(X0),X0)
& ! [X2] :
( r1_xboole_0(X2,X0)
| ~ r2_hidden(X2,sK320(X0)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK320]),skolemize(X1,sK320(X0))],[f18947]) ).
fof(f20825,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,[],[f19670]) ).
fof(f20826,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,[],[f20825]) ).
fof(f20827,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(sK501(X0,X1,X3,X4),u1_struct_0(k3_yellow_1(X1)))
& k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),sK501(X0,X1,X3,X4))) = X0
& m1_subset_1(sK502(X0,X1,X3,X4),X1)
& sK501(X0,X1,X3,X4) = k1_tarski(sK502(X0,X1,X3,X4))
& r2_hidden(sK502(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,[sK501,sK502]),skolemize(X7,sK501(X0,X1,X3,X4)),skolemize(X8,sK502(X0,X1,X3,X4))],[f20826]) ).
fof(f20896,plain,
l1_orders_2(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20897,plain,
v3_waybel_3(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20898,plain,
v3_lattice3(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20899,plain,
v4_orders_2(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20900,plain,
v3_orders_2(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20901,plain,
v2_orders_2(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20902,plain,
~ v3_struct_0(sK68),
inference(cnf_transformation,[],[f20055]) ).
fof(f20903,plain,
m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)),
inference(cnf_transformation,[],[f20055]) ).
fof(f20904,plain,
v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68)),
inference(cnf_transformation,[],[f20055]) ).
fof(f20905,plain,
v1_funct_1(sK69),
inference(cnf_transformation,[],[f20055]) ).
fof(f20906,plain,
k4_yellow_0(sK68) != k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK67))),sK68,k2_waybel22(sK67,sK68,sK69),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK67))))),
inference(cnf_transformation,[],[f20055]) ).
fof(f20912,plain,
! [X0] :
( ~ v3_lattice3(X0)
| v2_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17876]) ).
fof(f20913,plain,
! [X0] :
( ~ v3_lattice3(X0)
| v1_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17876]) ).
fof(f20915,plain,
! [X0] :
( ~ v2_yellow_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| u1_struct_0(X0) = k6_waybel_0(X0,k4_yellow_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17880]) ).
fof(f20925,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17895]) ).
fof(f20926,plain,
! [X0,X1] :
( r1_orders_2(X0,X1,k4_yellow_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17897]) ).
fof(f20927,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17898]) ).
fof(f20958,plain,
! [X0] : k1_zfmisc_1(X0) = k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))),
inference(cnf_transformation,[],[f17272]) ).
fof(f20981,plain,
! [X0] : l1_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f15126]) ).
fof(f21033,plain,
! [X0] : k3_yellow_1(X0) = k2_yellow_1(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f15095]) ).
fof(f21045,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,[],[f20080]) ).
fof(f21048,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,[],[f17953]) ).
fof(f21049,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,[],[f17953]) ).
fof(f21050,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,[],[f17953]) ).
fof(f21097,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,[],[f17971]) ).
fof(f21100,plain,
! [X0] :
( ~ v24_waybel_0(X0)
| ~ v2_orders_2(X0)
| ~ v1_lattice3(X0)
| v2_yellow_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f17977]) ).
fof(f21121,plain,
! [X2,X0,X1] :
( r2_hidden(X2,k6_waybel_0(X0,X1))
| ~ r1_orders_2(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20099]) ).
fof(f21182,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f20117]) ).
fof(f21188,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f471]) ).
fof(f21235,plain,
! [X0] :
( v2_yellow_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18097]) ).
fof(f21236,plain,
! [X0] :
( v1_yellow_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18097]) ).
fof(f21317,plain,
! [X0] :
( m1_subset_1(k3_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18129]) ).
fof(f21324,plain,
! [X0] :
( ~ v1_yellow_0(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| u1_struct_0(X0) = k7_waybel_0(X0,k3_yellow_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18140]) ).
fof(f21329,plain,
! [X2,X0,X1] :
( k6_waybel_0(X0,X1) = k7_waybel_0(k7_lattice3(X0),X2)
| X1 != X2
| ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18148]) ).
fof(f21331,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k2_yellow_0(X0,k7_waybel_0(X0,X1)) = X1
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18152]) ).
fof(f21334,plain,
! [X2,X0,X1] :
( k7_waybel_0(X0,X1) != k7_waybel_0(X0,X2)
| X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18156]) ).
fof(f21335,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X2,k7_waybel_0(X0,X1))
| r1_orders_2(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20143]) ).
fof(f21440,plain,
! [X0] : m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f486]) ).
fof(f21446,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f20169]) ).
fof(f21457,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f18226]) ).
fof(f21464,plain,
! [X0,X1] :
( m1_subset_1(k2_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18229]) ).
fof(f21750,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f20296]) ).
fof(f21897,plain,
! [X0] :
( ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| v24_waybel_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18382]) ).
fof(f22056,plain,
! [X0,X1] :
( ~ r1_yellow_0(X0,X1)
| k1_yellow_0(X0,X1) = k2_yellow_0(k7_lattice3(X0),X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18501]) ).
fof(f22135,plain,
! [X0,X1] :
( r1_yellow_0(X0,X1)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18543]) ).
fof(f22193,plain,
! [X0] :
( v3_lattice3(k7_lattice3(X0))
| ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f20405]) ).
fof(f22221,plain,
! [X0] :
( ~ l1_orders_2(X0)
| u1_struct_0(X0) = u1_struct_0(k7_lattice3(X0)) ),
inference(cnf_transformation,[],[f18578]) ).
fof(f22222,plain,
! [X0] :
( l1_orders_2(k7_lattice3(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18579]) ).
fof(f22227,plain,
! [X0] :
( ~ v3_struct_0(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18582]) ).
fof(f22228,plain,
! [X0] :
( v4_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18584]) ).
fof(f22229,plain,
! [X0] :
( v3_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18584]) ).
fof(f22230,plain,
! [X0] :
( v2_orders_2(k7_lattice3(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f18584]) ).
fof(f22543,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,[],[f20480]) ).
fof(f22584,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,[],[f20499]) ).
fof(f22773,plain,
! [X0] :
( k1_xboole_0 = X0
| r2_hidden(sK320(X0),X0) ),
inference(cnf_transformation,[],[f20563]) ).
fof(f23734,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f3551]) ).
fof(f23846,plain,
! [X2,X3,X0,X1,X4] :
( ~ r2_hidden(X0,a_4_1_waybel22(X1,X2,X3,X4))
| r2_hidden(sK502(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,[],[f20827]) ).
fof(f24203,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,[],[f20958,f21033]) ).
fof(f24205,plain,
k4_yellow_0(sK68) != k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))),
inference(definition_unfolding,[],[f20906,f21033,f21033]) ).
fof(f24207,plain,
! [X0] :
( ~ l1_orders_2(X0)
| k4_yellow_0(X0) = k2_yellow_0(X0,np__0) ),
inference(definition_unfolding,[],[f20927,f23734]) ).
fof(f24268,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,[],[f21045,f21033,f21033,f21033,f21033]) ).
fof(f24269,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,[],[f21049,f21033]) ).
fof(f24270,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,[],[f21048,f21033]) ).
fof(f24327,plain,
! [X0] : m1_subset_1(np__0,k1_zfmisc_1(X0)),
inference(definition_unfolding,[],[f21440,f23734]) ).
fof(f24334,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| np__0 != X0 ),
inference(definition_unfolding,[],[f21446,f23734]) ).
fof(f24573,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,[],[f22584,f21033]) ).
fof(f24620,plain,
! [X0] :
( r2_hidden(sK320(X0),X0)
| np__0 = X0 ),
inference(definition_unfolding,[],[f22773,f23734]) ).
fof(f25059,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,[],[f24268]) ).
fof(f25062,plain,
! [X2,X0] :
( ~ m1_subset_1(X2,u1_struct_0(k7_lattice3(X0)))
| k6_waybel_0(X0,X2) = k7_waybel_0(k7_lattice3(X0),X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f21329]) ).
fof(f25073,plain,
! [X2] : ~ r2_hidden(X2,np__0),
inference(equality_resolution,[],[f24334]) ).
fof(f25132,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,[],[f24573]) ).
fof(f25462,plain,
( v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(resolution,[],[f21050,f20904]) ).
fof(f25463,plain,
( ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25462,f20902]) ).
fof(f25464,plain,
( ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25463,f20901]) ).
fof(f25465,plain,
( ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25464,f20900]) ).
fof(f25466,plain,
( ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25465,f20899]) ).
fof(f25467,plain,
( ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25466,f20898]) ).
fof(f25468,plain,
( ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25467,f20897]) ).
fof(f25469,plain,
( ~ v1_funct_1(sK69)
| v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25468,f20896]) ).
fof(f25470,plain,
( v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f25469,f20905]) ).
fof(f25472,definition,
( spl541_12
<=> m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_12])],[avatar_definition]) ).
fof(f25474,plain,
( ~ m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| spl541_12 ),
inference(avatar_component_clause,[],[f25472]) ).
fof(f25476,definition,
( spl541_13
<=> v1_funct_1(k2_waybel22(sK67,sK68,sK69)) ),
introduced(definition,[new_symbols(definition,[spl541_13])],[avatar_definition]) ).
fof(f25478,plain,
( v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ spl541_13 ),
inference(avatar_component_clause,[],[f25476]) ).
fof(f25479,plain,
( ~ spl541_12
| spl541_13 ),
inference(avatar_split_clause,[],[f25470,f25476,f25472]) ).
fof(f25480,plain,
m1_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)),
inference(resolution,[],[f21750,f20903]) ).
fof(f25481,plain,
( $false
| spl541_12 ),
inference(forward_subsumption_resolution,[],[f25480,f25474]) ).
fof(f25482,plain,
spl541_12,
inference(avatar_contradiction_clause,[],[f25481]) ).
fof(f25486,plain,
k4_yellow_0(sK68) = k2_yellow_0(sK68,np__0),
inference(resolution,[],[f24207,f20896]) ).
fof(f25498,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))))
| ~ v1_funct_1(k2_waybel22(X1,X2,X3))
| k1_yellow_0(X2,a_4_0_waybel22(X1,X2,X3,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))),X2,k2_waybel22(X1,X2,X3),X0)
| ~ m2_relset_1(k2_waybel22(X1,X2,X3),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))),u1_struct_0(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))
| 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)
| 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))
| ~ m1_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2)) ),
inference(resolution,[],[f25059,f24269]) ).
fof(f25499,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))))
| ~ v1_funct_1(k2_waybel22(X1,X2,X3))
| k1_yellow_0(X2,a_4_0_waybel22(X1,X2,X3,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))),X2,k2_waybel22(X1,X2,X3),X0)
| ~ m2_relset_1(k2_waybel22(X1,X2,X3),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))),u1_struct_0(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))
| 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)
| ~ m1_relset_1(X3,k1_waybel22(X1),u1_struct_0(X2)) ),
inference(duplicate_literal_removal,[],[f25498]) ).
fof(f25500,plain,
! [X2,X3,X0,X1] :
( ~ m2_relset_1(k2_waybel22(X1,X2,X3),u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))),u1_struct_0(X2))
| ~ v1_funct_1(k2_waybel22(X1,X2,X3))
| k1_yellow_0(X2,a_4_0_waybel22(X1,X2,X3,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))),X2,k2_waybel22(X1,X2,X3),X0)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))))
| ~ 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))
| 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) ),
inference(forward_subsumption_resolution,[],[f25499,f21750]) ).
fof(f25507,plain,
u1_struct_0(sK68) = u1_struct_0(k7_lattice3(sK68)),
inference(resolution,[],[f22221,f20896]) ).
fof(f25517,definition,
( spl541_14
<=> l1_orders_2(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_14])],[avatar_definition]) ).
fof(f25518,plain,
( l1_orders_2(k7_lattice3(sK68))
| ~ spl541_14 ),
inference(avatar_component_clause,[],[f25517]) ).
fof(f25519,plain,
( ~ l1_orders_2(k7_lattice3(sK68))
| spl541_14 ),
inference(avatar_component_clause,[],[f25517]) ).
fof(f25525,definition,
( spl541_16
<=> v3_lattice3(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_16])],[avatar_definition]) ).
fof(f25526,plain,
( v3_lattice3(k7_lattice3(sK68))
| ~ spl541_16 ),
inference(avatar_component_clause,[],[f25525]) ).
fof(f25527,plain,
( ~ v3_lattice3(k7_lattice3(sK68))
| spl541_16 ),
inference(avatar_component_clause,[],[f25525]) ).
fof(f25529,definition,
( spl541_17
<=> v4_orders_2(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_17])],[avatar_definition]) ).
fof(f25530,plain,
( v4_orders_2(k7_lattice3(sK68))
| ~ spl541_17 ),
inference(avatar_component_clause,[],[f25529]) ).
fof(f25531,plain,
( ~ v4_orders_2(k7_lattice3(sK68))
| spl541_17 ),
inference(avatar_component_clause,[],[f25529]) ).
fof(f25533,definition,
( spl541_18
<=> v3_orders_2(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_18])],[avatar_definition]) ).
fof(f25534,plain,
( v3_orders_2(k7_lattice3(sK68))
| ~ spl541_18 ),
inference(avatar_component_clause,[],[f25533]) ).
fof(f25535,plain,
( ~ v3_orders_2(k7_lattice3(sK68))
| spl541_18 ),
inference(avatar_component_clause,[],[f25533]) ).
fof(f25537,definition,
( spl541_19
<=> v2_orders_2(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_19])],[avatar_definition]) ).
fof(f25538,plain,
( v2_orders_2(k7_lattice3(sK68))
| ~ spl541_19 ),
inference(avatar_component_clause,[],[f25537]) ).
fof(f25539,plain,
( ~ v2_orders_2(k7_lattice3(sK68))
| spl541_19 ),
inference(avatar_component_clause,[],[f25537]) ).
fof(f25541,definition,
( spl541_20
<=> v3_struct_0(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_20])],[avatar_definition]) ).
fof(f25542,plain,
( ~ v3_struct_0(k7_lattice3(sK68))
| spl541_20 ),
inference(avatar_component_clause,[],[f25541]) ).
fof(f25543,plain,
( v3_struct_0(k7_lattice3(sK68))
| ~ spl541_20 ),
inference(avatar_component_clause,[],[f25541]) ).
fof(f25577,plain,
( ~ l1_orders_2(sK68)
| spl541_14 ),
inference(resolution,[],[f25519,f22222]) ).
fof(f25578,plain,
( $false
| spl541_14 ),
inference(forward_subsumption_resolution,[],[f25577,f20896]) ).
fof(f25579,plain,
spl541_14,
inference(avatar_contradiction_clause,[],[f25578]) ).
fof(f25624,plain,
( v3_struct_0(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_20 ),
inference(resolution,[],[f22227,f25543]) ).
fof(f25625,plain,
( ~ l1_orders_2(sK68)
| ~ spl541_20 ),
inference(forward_subsumption_resolution,[],[f25624,f20902]) ).
fof(f25626,plain,
( $false
| ~ spl541_20 ),
inference(forward_subsumption_resolution,[],[f25625,f20896]) ).
fof(f25627,plain,
~ spl541_20,
inference(avatar_contradiction_clause,[],[f25626]) ).
fof(f25681,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(k2_waybel22(X0,X1,X2))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),X3) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X3))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))))
| ~ 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)
| 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,[],[f25500,f24270]) ).
fof(f25683,plain,
! [X2,X3,X0,X1] :
( ~ v1_funct_1(k2_waybel22(X0,X1,X2))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),X3) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X3))
| ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))))
| ~ 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)
| ~ m1_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(duplicate_literal_removal,[],[f25681]) ).
fof(f25684,plain,
! [X2,X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))))
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),X3) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X3))
| ~ v1_funct_1(k2_waybel22(X0,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))
| 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(forward_subsumption_resolution,[],[f25683,f21750]) ).
fof(f25685,plain,
k4_yellow_0(sK68) != k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)),
inference(superposition,[],[f24205,f24203]) ).
fof(f25701,plain,
( v1_lattice3(sK68)
| v3_struct_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(resolution,[],[f20913,f20898]) ).
fof(f25704,plain,
( v1_lattice3(sK68)
| ~ l1_orders_2(sK68) ),
inference(forward_subsumption_resolution,[],[f25701,f20902]) ).
fof(f25705,plain,
v1_lattice3(sK68),
inference(forward_subsumption_resolution,[],[f25704,f20896]) ).
fof(f25944,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k7_waybel_0(k7_lattice3(sK68),X0) = k6_waybel_0(sK68,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| v3_struct_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(superposition,[],[f25062,f25507]) ).
fof(f25946,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k7_waybel_0(k7_lattice3(sK68),X0) = k6_waybel_0(sK68,X0)
| v3_struct_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(duplicate_literal_removal,[],[f25944]) ).
fof(f25948,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k7_waybel_0(k7_lattice3(sK68),X0) = k6_waybel_0(sK68,X0)
| ~ l1_orders_2(sK68) ),
inference(forward_subsumption_resolution,[],[f25946,f20902]) ).
fof(f25953,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k7_waybel_0(k7_lattice3(sK68),X0) = k6_waybel_0(sK68,X0) ),
inference(forward_subsumption_resolution,[],[f25948,f20896]) ).
fof(f25960,plain,
( v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| v24_waybel_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(resolution,[],[f21897,f20898]) ).
fof(f25964,plain,
( ~ v2_orders_2(sK68)
| v24_waybel_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(forward_subsumption_resolution,[],[f25960,f20902]) ).
fof(f25966,plain,
( v24_waybel_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(forward_subsumption_resolution,[],[f25964,f20901]) ).
fof(f25967,plain,
v24_waybel_0(sK68),
inference(forward_subsumption_resolution,[],[f25966,f20896]) ).
fof(f26202,plain,
( ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_17 ),
inference(resolution,[],[f25531,f22228]) ).
fof(f26205,plain,
( ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_17 ),
inference(forward_subsumption_resolution,[],[f26202,f20901]) ).
fof(f26208,plain,
( ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_17 ),
inference(forward_subsumption_resolution,[],[f26205,f20900]) ).
fof(f26209,plain,
( ~ l1_orders_2(sK68)
| spl541_17 ),
inference(forward_subsumption_resolution,[],[f26208,f20899]) ).
fof(f26210,plain,
( $false
| spl541_17 ),
inference(forward_subsumption_resolution,[],[f26209,f20896]) ).
fof(f26211,plain,
spl541_17,
inference(avatar_contradiction_clause,[],[f26210]) ).
fof(f26212,plain,
( ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_18 ),
inference(resolution,[],[f25535,f22229]) ).
fof(f26215,plain,
( ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_18 ),
inference(forward_subsumption_resolution,[],[f26212,f20901]) ).
fof(f26218,plain,
( ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_18 ),
inference(forward_subsumption_resolution,[],[f26215,f20900]) ).
fof(f26219,plain,
( ~ l1_orders_2(sK68)
| spl541_18 ),
inference(forward_subsumption_resolution,[],[f26218,f20899]) ).
fof(f26220,plain,
( $false
| spl541_18 ),
inference(forward_subsumption_resolution,[],[f26219,f20896]) ).
fof(f26221,plain,
spl541_18,
inference(avatar_contradiction_clause,[],[f26220]) ).
fof(f26225,plain,
( ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_19 ),
inference(resolution,[],[f25539,f22230]) ).
fof(f26228,plain,
( ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_19 ),
inference(forward_subsumption_resolution,[],[f26225,f20901]) ).
fof(f26231,plain,
( ~ v4_orders_2(sK68)
| ~ l1_orders_2(sK68)
| spl541_19 ),
inference(forward_subsumption_resolution,[],[f26228,f20900]) ).
fof(f26232,plain,
( ~ l1_orders_2(sK68)
| spl541_19 ),
inference(forward_subsumption_resolution,[],[f26231,f20899]) ).
fof(f26233,plain,
( $false
| spl541_19 ),
inference(forward_subsumption_resolution,[],[f26232,f20896]) ).
fof(f26234,plain,
spl541_19,
inference(avatar_contradiction_clause,[],[f26233]) ).
fof(f26279,definition,
( spl541_60
<=> v2_yellow_0(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_60])],[avatar_definition]) ).
fof(f26280,plain,
( v2_yellow_0(k7_lattice3(sK68))
| ~ spl541_60 ),
inference(avatar_component_clause,[],[f26279]) ).
fof(f26281,plain,
( ~ v2_yellow_0(k7_lattice3(sK68))
| spl541_60 ),
inference(avatar_component_clause,[],[f26279]) ).
fof(f26287,plain,
( v3_struct_0(sK68)
| ~ v3_lattice3(sK68)
| ~ l1_orders_2(sK68)
| spl541_60 ),
inference(resolution,[],[f26281,f21235]) ).
fof(f26288,plain,
( ~ v3_lattice3(sK68)
| ~ l1_orders_2(sK68)
| spl541_60 ),
inference(forward_subsumption_resolution,[],[f26287,f20902]) ).
fof(f26289,plain,
( ~ l1_orders_2(sK68)
| spl541_60 ),
inference(forward_subsumption_resolution,[],[f26288,f20898]) ).
fof(f26290,plain,
( $false
| spl541_60 ),
inference(forward_subsumption_resolution,[],[f26289,f20896]) ).
fof(f26291,plain,
spl541_60,
inference(avatar_contradiction_clause,[],[f26290]) ).
fof(f26292,plain,
( v3_struct_0(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| u1_struct_0(k7_lattice3(sK68)) = k6_waybel_0(k7_lattice3(sK68),k4_yellow_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ spl541_60 ),
inference(resolution,[],[f26280,f20915]) ).
fof(f26295,plain,
( ~ v4_orders_2(k7_lattice3(sK68))
| u1_struct_0(k7_lattice3(sK68)) = k6_waybel_0(k7_lattice3(sK68),k4_yellow_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68))
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f26292,f25542]) ).
fof(f26297,plain,
( u1_struct_0(k7_lattice3(sK68)) = k6_waybel_0(k7_lattice3(sK68),k4_yellow_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f26295,f25530]) ).
fof(f26299,plain,
( u1_struct_0(k7_lattice3(sK68)) = k6_waybel_0(k7_lattice3(sK68),k4_yellow_0(k7_lattice3(sK68)))
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f26297,f25518]) ).
fof(f26301,plain,
( u1_struct_0(sK68) = k6_waybel_0(k7_lattice3(sK68),k4_yellow_0(k7_lattice3(sK68)))
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_demodulation,[],[f26299,f25507]) ).
fof(f26405,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),X0)) = X0
| v3_struct_0(k7_lattice3(sK68))
| ~ v2_orders_2(k7_lattice3(sK68))
| ~ v3_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) ),
inference(superposition,[],[f21331,f25507]) ).
fof(f26412,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),X0)) = X0
| ~ v2_orders_2(k7_lattice3(sK68))
| ~ v3_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26405,f25542]) ).
fof(f26417,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),X0)) = X0
| ~ v3_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26412,f25538]) ).
fof(f26421,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),X0)) = X0
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26417,f25534]) ).
fof(f26425,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),X0)) = X0
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26421,f25530]) ).
fof(f26429,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),X0)) = X0 )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26425,f25518]) ).
fof(f26469,plain,
! [X2,X0,X1] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))))
| ~ v1_funct_1(k2_waybel22(X0,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))
| 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)
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0))))) ),
inference(resolution,[],[f25684,f20925]) ).
fof(f26473,plain,
! [X2,X0,X1] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))))))
| ~ v1_funct_1(k2_waybel22(X0,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))
| 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(forward_subsumption_resolution,[],[f26469,f20981]) ).
fof(f26475,plain,
! [X2,X0,X1] :
( ~ v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ v1_funct_1(k2_waybel22(X0,X1,X2))
| ~ v1_funct_1(X2)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X0)))),X1,k2_waybel22(X0,X1,X2),k1_zfmisc_1(X0)) = k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,k1_zfmisc_1(X0)))
| ~ 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(forward_demodulation,[],[f26473,f24203]) ).
fof(f26688,plain,
( ~ v3_lattice3(sK68)
| v3_struct_0(sK68)
| ~ l1_orders_2(sK68)
| spl541_16 ),
inference(resolution,[],[f25527,f22193]) ).
fof(f26689,plain,
( v3_struct_0(sK68)
| ~ l1_orders_2(sK68)
| spl541_16 ),
inference(forward_subsumption_resolution,[],[f26688,f20898]) ).
fof(f26690,plain,
( ~ l1_orders_2(sK68)
| spl541_16 ),
inference(forward_subsumption_resolution,[],[f26689,f20902]) ).
fof(f26691,plain,
( $false
| spl541_16 ),
inference(forward_subsumption_resolution,[],[f26690,f20896]) ).
fof(f26692,plain,
spl541_16,
inference(avatar_contradiction_clause,[],[f26691]) ).
fof(f26929,plain,
( k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),k4_yellow_0(sK68)))
| ~ l1_orders_2(sK68)
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(resolution,[],[f26429,f20925]) ).
fof(f26934,plain,
( k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),k7_waybel_0(k7_lattice3(sK68),k4_yellow_0(sK68)))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26929,f20896]) ).
fof(f26963,plain,
( m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(superposition,[],[f21464,f26934]) ).
fof(f26965,plain,
! [X0] :
( m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) ),
inference(superposition,[],[f21464,f25507]) ).
fof(f26972,plain,
( ! [X0] : m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| ~ spl541_14 ),
inference(forward_subsumption_resolution,[],[f26965,f25518]) ).
fof(f26974,plain,
( m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f26963,f25518]) ).
fof(f26980,plain,
( m1_subset_1(k4_yellow_0(sK68),u1_struct_0(sK68))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_demodulation,[],[f26974,f25507]) ).
fof(f26988,plain,
! [X0] :
( v3_struct_0(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| u1_struct_0(k7_lattice3(X0)) = k7_waybel_0(k7_lattice3(X0),k3_yellow_0(k7_lattice3(X0)))
| ~ l1_orders_2(k7_lattice3(X0))
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f21324,f21236]) ).
fof(f26991,plain,
! [X0] :
( v3_struct_0(k7_lattice3(X0))
| ~ v4_orders_2(k7_lattice3(X0))
| u1_struct_0(k7_lattice3(X0)) = k7_waybel_0(k7_lattice3(X0),k3_yellow_0(k7_lattice3(X0)))
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f26988,f22222]) ).
fof(f26993,plain,
! [X0] :
( ~ v4_orders_2(k7_lattice3(X0))
| u1_struct_0(k7_lattice3(X0)) = k7_waybel_0(k7_lattice3(X0),k3_yellow_0(k7_lattice3(X0)))
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(forward_subsumption_resolution,[],[f26991,f22227]) ).
fof(f26999,plain,
( u1_struct_0(k7_lattice3(sK68)) = k7_waybel_0(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)))
| v3_struct_0(sK68)
| ~ v3_lattice3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_17 ),
inference(resolution,[],[f26993,f25530]) ).
fof(f27004,plain,
( u1_struct_0(k7_lattice3(sK68)) = k7_waybel_0(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)))
| ~ v3_lattice3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_17 ),
inference(forward_subsumption_resolution,[],[f26999,f20902]) ).
fof(f27006,plain,
( u1_struct_0(k7_lattice3(sK68)) = k7_waybel_0(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)))
| ~ l1_orders_2(sK68)
| ~ spl541_17 ),
inference(forward_subsumption_resolution,[],[f27004,f20898]) ).
fof(f27008,plain,
( u1_struct_0(k7_lattice3(sK68)) = k7_waybel_0(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)))
| ~ spl541_17 ),
inference(forward_subsumption_resolution,[],[f27006,f20896]) ).
fof(f27010,plain,
( u1_struct_0(sK68) = k7_waybel_0(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)))
| ~ spl541_17 ),
inference(forward_demodulation,[],[f27008,f25507]) ).
fof(f27013,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| k3_yellow_0(k7_lattice3(sK68)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ m1_subset_1(k3_yellow_0(k7_lattice3(sK68)),u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ v2_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17 ),
inference(superposition,[],[f21334,f27010]) ).
fof(f27014,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| k3_yellow_0(k7_lattice3(sK68)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ v2_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17 ),
inference(forward_subsumption_resolution,[],[f27013,f21317]) ).
fof(f27017,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| k3_yellow_0(k7_lattice3(sK68)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ v2_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f27014,f25542]) ).
fof(f27028,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| k3_yellow_0(k7_lattice3(sK68)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f27017,f25538]) ).
fof(f27030,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| k3_yellow_0(k7_lattice3(sK68)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f27028,f25530]) ).
fof(f27032,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| k3_yellow_0(k7_lattice3(sK68)) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f27030,f25518]) ).
fof(f27034,plain,
( ! [X0] :
( u1_struct_0(sK68) != k7_waybel_0(k7_lattice3(sK68),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| k3_yellow_0(k7_lattice3(sK68)) = X0 )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_19
| spl541_20 ),
inference(forward_demodulation,[],[f27032,f25507]) ).
fof(f27097,plain,
! [X0] :
( r2_hidden(np__0,k1_zfmisc_1(X0))
| v1_xboole_0(k1_zfmisc_1(X0)) ),
inference(resolution,[],[f21182,f24327]) ).
fof(f27115,plain,
! [X0] : r2_hidden(np__0,k1_zfmisc_1(X0)),
inference(forward_subsumption_resolution,[],[f27097,f21188]) ).
fof(f27987,plain,
( k7_waybel_0(k7_lattice3(sK68),k4_yellow_0(sK68)) = k6_waybel_0(sK68,k4_yellow_0(sK68))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(resolution,[],[f25953,f26980]) ).
fof(f27995,plain,
( u1_struct_0(sK68) != k6_waybel_0(sK68,k4_yellow_0(sK68))
| ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k3_yellow_0(k7_lattice3(sK68))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(superposition,[],[f27034,f27987]) ).
fof(f28002,plain,
( u1_struct_0(sK68) != k6_waybel_0(sK68,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = k3_yellow_0(k7_lattice3(sK68))
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f27995,f26980]) ).
fof(f28007,definition,
( spl541_143
<=> k4_yellow_0(sK68) = k3_yellow_0(k7_lattice3(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_143])],[avatar_definition]) ).
fof(f28009,plain,
( k4_yellow_0(sK68) = k3_yellow_0(k7_lattice3(sK68))
| ~ spl541_143 ),
inference(avatar_component_clause,[],[f28007]) ).
fof(f28011,definition,
( spl541_144
<=> u1_struct_0(sK68) = k6_waybel_0(sK68,k4_yellow_0(sK68)) ),
introduced(definition,[new_symbols(definition,[spl541_144])],[avatar_definition]) ).
fof(f28013,plain,
( u1_struct_0(sK68) != k6_waybel_0(sK68,k4_yellow_0(sK68))
| spl541_144 ),
inference(avatar_component_clause,[],[f28011]) ).
fof(f28014,plain,
( spl541_143
| ~ spl541_144
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20 ),
inference(avatar_split_clause,[],[f28002,f25541,f25537,f25533,f25529,f25517,f28011,f28007]) ).
fof(f29245,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ m1_subset_1(k4_yellow_0(k7_lattice3(sK68)),u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(superposition,[],[f21121,f26301]) ).
fof(f29249,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29245,f20925]) ).
fof(f29251,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29249,f25542]) ).
fof(f29253,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29251,f25518]) ).
fof(f29255,plain,
( ! [X0] :
( ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(k7_lattice3(sK68)))
| r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_demodulation,[],[f29253,f25507]) ).
fof(f29257,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ v2_yellow_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(resolution,[],[f29255,f20926]) ).
fof(f29259,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ v2_yellow_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29257,f25542]) ).
fof(f29260,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ v2_yellow_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29259,f25530]) ).
fof(f29261,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29260,f26280]) ).
fof(f29262,plain,
( ! [X0] :
( r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_subsumption_resolution,[],[f29261,f25518]) ).
fof(f29263,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(forward_demodulation,[],[f29262,f25507]) ).
fof(f29264,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| r2_hidden(X0,u1_struct_0(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60 ),
inference(duplicate_literal_removal,[],[f29263]) ).
fof(f29528,definition,
( spl541_180
<=> v2_yellow_0(sK68) ),
introduced(definition,[new_symbols(definition,[spl541_180])],[avatar_definition]) ).
fof(f29529,plain,
( v2_yellow_0(sK68)
| ~ spl541_180 ),
inference(avatar_component_clause,[],[f29528]) ).
fof(f29530,plain,
( ~ v2_yellow_0(sK68)
| spl541_180 ),
inference(avatar_component_clause,[],[f29528]) ).
fof(f29854,plain,
( ~ v2_orders_2(sK68)
| ~ v1_lattice3(sK68)
| v2_yellow_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(resolution,[],[f21100,f25967]) ).
fof(f29859,plain,
( ~ v1_lattice3(sK68)
| v2_yellow_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(forward_subsumption_resolution,[],[f29854,f20901]) ).
fof(f29862,plain,
( v2_yellow_0(sK68)
| ~ l1_orders_2(sK68) ),
inference(forward_subsumption_resolution,[],[f29859,f25705]) ).
fof(f29865,plain,
( ~ l1_orders_2(sK68)
| spl541_180 ),
inference(forward_subsumption_resolution,[],[f29862,f29530]) ).
fof(f29868,plain,
( $false
| spl541_180 ),
inference(forward_subsumption_resolution,[],[f29865,f20896]) ).
fof(f29869,plain,
spl541_180,
inference(avatar_contradiction_clause,[],[f29868]) ).
fof(f29900,plain,
( v3_struct_0(sK68)
| ~ v4_orders_2(sK68)
| u1_struct_0(sK68) = k6_waybel_0(sK68,k4_yellow_0(sK68))
| ~ l1_orders_2(sK68)
| ~ spl541_180 ),
inference(resolution,[],[f29529,f20915]) ).
fof(f29903,plain,
( ~ v4_orders_2(sK68)
| u1_struct_0(sK68) = k6_waybel_0(sK68,k4_yellow_0(sK68))
| ~ l1_orders_2(sK68)
| ~ spl541_180 ),
inference(forward_subsumption_resolution,[],[f29900,f20902]) ).
fof(f29907,plain,
( u1_struct_0(sK68) = k6_waybel_0(sK68,k4_yellow_0(sK68))
| ~ l1_orders_2(sK68)
| ~ spl541_180 ),
inference(forward_subsumption_resolution,[],[f29903,f20899]) ).
fof(f29911,plain,
( ~ l1_orders_2(sK68)
| spl541_144
| ~ spl541_180 ),
inference(forward_subsumption_resolution,[],[f29907,f28013]) ).
fof(f29915,plain,
( $false
| spl541_144
| ~ spl541_180 ),
inference(forward_subsumption_resolution,[],[f29911,f20896]) ).
fof(f29916,plain,
( spl541_144
| ~ spl541_180 ),
inference(avatar_contradiction_clause,[],[f29915]) ).
fof(f30166,plain,
( ! [X0] :
( ~ r2_hidden(X0,u1_struct_0(sK68))
| r1_orders_2(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)),X0)
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ m1_subset_1(k3_yellow_0(k7_lattice3(sK68)),u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17 ),
inference(superposition,[],[f21335,f27010]) ).
fof(f30172,plain,
( ! [X0] :
( ~ r2_hidden(X0,u1_struct_0(sK68))
| r1_orders_2(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)),X0)
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| v3_struct_0(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17 ),
inference(forward_subsumption_resolution,[],[f30166,f21317]) ).
fof(f30178,plain,
( ! [X0] :
( ~ r2_hidden(X0,u1_struct_0(sK68))
| r1_orders_2(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)),X0)
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_17
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f30172,f25542]) ).
fof(f30184,plain,
( ! [X0] :
( ~ r2_hidden(X0,u1_struct_0(sK68))
| r1_orders_2(k7_lattice3(sK68),k3_yellow_0(k7_lattice3(sK68)),X0)
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| spl541_20 ),
inference(forward_subsumption_resolution,[],[f30178,f25518]) ).
fof(f30189,plain,
( ! [X0] :
( r1_orders_2(k7_lattice3(sK68),k4_yellow_0(sK68),X0)
| ~ r2_hidden(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_143 ),
inference(forward_demodulation,[],[f30184,f28009]) ).
fof(f30194,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| r1_orders_2(k7_lattice3(sK68),k4_yellow_0(sK68),X0)
| ~ r2_hidden(X0,u1_struct_0(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_143 ),
inference(forward_demodulation,[],[f30189,f25507]) ).
fof(f30198,plain,
( ! [X0] :
( r1_orders_2(k7_lattice3(sK68),k4_yellow_0(sK68),X0)
| ~ m1_subset_1(X0,u1_struct_0(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f30194,f29264]) ).
fof(f30203,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = X0
| ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(resolution,[],[f30198,f21097]) ).
fof(f30204,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = X0
| ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68)) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f30203,f25530]) ).
fof(f30206,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = X0
| ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f30204,f25518]) ).
fof(f30208,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_demodulation,[],[f30206,f25507]) ).
fof(f30210,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = X0
| ~ m1_subset_1(X0,u1_struct_0(k7_lattice3(sK68))) )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f30208,f26980]) ).
fof(f30212,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| k4_yellow_0(sK68) = X0 )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_demodulation,[],[f30210,f25507]) ).
fof(f30213,plain,
( ! [X0] :
( ~ r1_orders_2(k7_lattice3(sK68),X0,k4_yellow_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(sK68))
| k4_yellow_0(sK68) = X0 )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(duplicate_literal_removal,[],[f30212]) ).
fof(f30712,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,k2_yellow_0(X2,X1),X0)
| v3_struct_0(X2)
| ~ v2_orders_2(X2)
| ~ l1_orders_2(X2)
| ~ m1_subset_1(k2_yellow_0(X2,X1),u1_struct_0(X2))
| ~ m1_subset_1(X0,u1_struct_0(X2)) ),
inference(resolution,[],[f21457,f22543]) ).
fof(f30722,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,k2_yellow_0(X2,X1),X0)
| v3_struct_0(X2)
| ~ m1_subset_1(k2_yellow_0(X2,X1),u1_struct_0(X2)) ),
inference(duplicate_literal_removal,[],[f30712]) ).
fof(f30730,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,k2_yellow_0(X2,X1),X0)
| v3_struct_0(X2) ),
inference(forward_subsumption_resolution,[],[f30722,f21464]) ).
fof(f30738,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,k2_yellow_0(X2,X1),X0)
| v3_struct_0(X2) ),
inference(forward_subsumption_resolution,[],[f30730,f20913]) ).
fof(f30746,plain,
! [X2,X0,X1] :
( r1_orders_2(X2,k2_yellow_0(X2,X1),X0)
| ~ 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,[],[f30738,f20912]) ).
fof(f30824,plain,
( ~ v1_funct_1(k2_waybel22(sK67,sK68,sK69))
| ~ v1_funct_1(sK69)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68) ),
inference(resolution,[],[f26475,f20904]) ).
fof(f30832,plain,
( ~ v1_funct_1(sK69)
| k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30824,f25478]) ).
fof(f30835,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30832,f20905]) ).
fof(f30837,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30835,f20903]) ).
fof(f30839,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30837,f20902]) ).
fof(f30841,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30839,f20901]) ).
fof(f30843,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30841,f20900]) ).
fof(f30844,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30843,f20899]) ).
fof(f30845,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30844,f20898]) ).
fof(f30846,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ l1_orders_2(sK68)
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30845,f20897]) ).
fof(f30847,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))),sK68,k2_waybel22(sK67,sK68,sK69),k1_zfmisc_1(sK67)) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ spl541_13 ),
inference(forward_subsumption_resolution,[],[f30846,f20896]) ).
fof(f30848,plain,
( k4_yellow_0(sK68) != k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ spl541_13 ),
inference(superposition,[],[f25685,f30847]) ).
fof(f34510,plain,
! [X0,X1] :
( k1_yellow_0(X0,X1) = k2_yellow_0(k7_lattice3(X0),X1)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(resolution,[],[f22056,f22135]) ).
fof(f34520,plain,
! [X0,X1] :
( ~ v3_lattice3(X0)
| v3_struct_0(X0)
| ~ l1_orders_2(X0)
| ~ v4_orders_2(X0)
| k1_yellow_0(X0,X1) = k2_yellow_0(k7_lattice3(X0),X1) ),
inference(duplicate_literal_removal,[],[f34510]) ).
fof(f34558,plain,
! [X0] :
( v3_struct_0(sK68)
| ~ l1_orders_2(sK68)
| ~ v4_orders_2(sK68)
| k1_yellow_0(sK68,X0) = k2_yellow_0(k7_lattice3(sK68),X0) ),
inference(resolution,[],[f34520,f20898]) ).
fof(f34577,plain,
! [X0] :
( ~ l1_orders_2(sK68)
| ~ v4_orders_2(sK68)
| k1_yellow_0(sK68,X0) = k2_yellow_0(k7_lattice3(sK68),X0) ),
inference(forward_subsumption_resolution,[],[f34558,f20902]) ).
fof(f34587,plain,
! [X0] :
( ~ v4_orders_2(sK68)
| k1_yellow_0(sK68,X0) = k2_yellow_0(k7_lattice3(sK68),X0) ),
inference(forward_subsumption_resolution,[],[f34577,f20896]) ).
fof(f34596,plain,
! [X0] : k1_yellow_0(sK68,X0) = k2_yellow_0(k7_lattice3(sK68),X0),
inference(forward_subsumption_resolution,[],[f34587,f20899]) ).
fof(f35208,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK502(sK320(a_4_1_waybel22(X0,X1,X2,X3)),X0,X2,X3),X3)
| np__0 = a_4_1_waybel22(X0,X1,X2,X3)
| 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))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_subset_1(X3,k1_zfmisc_1(X0)) ),
inference(resolution,[],[f24620,f23846]) ).
fof(f35273,plain,
! [X2,X0,X1] :
( np__0 = a_4_1_waybel22(X0,X1,X2,np__0)
| 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))
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1))
| ~ m1_subset_1(np__0,k1_zfmisc_1(X0)) ),
inference(resolution,[],[f35208,f25073]) ).
fof(f35285,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)
| np__0 = a_4_1_waybel22(X0,X1,X2,np__0)
| ~ m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) ),
inference(forward_subsumption_resolution,[],[f35273,f24327]) ).
fof(f35289,plain,
( v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(resolution,[],[f35285,f20904]) ).
fof(f35300,plain,
( ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35289,f20902]) ).
fof(f35304,plain,
( ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35300,f20901]) ).
fof(f35306,plain,
( ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35304,f20900]) ).
fof(f35308,plain,
( ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35306,f20899]) ).
fof(f35310,plain,
( ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35308,f20898]) ).
fof(f35312,plain,
( ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35310,f20897]) ).
fof(f35313,plain,
( ~ v1_funct_1(sK69)
| np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35312,f20896]) ).
fof(f35314,plain,
( np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68)) ),
inference(forward_subsumption_resolution,[],[f35313,f20905]) ).
fof(f35315,plain,
np__0 = a_4_1_waybel22(sK67,sK68,sK69,np__0),
inference(forward_subsumption_resolution,[],[f35314,f20903]) ).
fof(f35320,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ m1_subset_1(np__0,k1_zfmisc_1(sK67))
| ~ r2_hidden(np__0,X0)
| v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(superposition,[],[f25132,f35315]) ).
fof(f35324,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| v3_struct_0(sK68)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35320,f24327]) ).
fof(f35325,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v2_orders_2(sK68)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35324,f20902]) ).
fof(f35326,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v3_orders_2(sK68)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35325,f20901]) ).
fof(f35327,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v4_orders_2(sK68)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35326,f20900]) ).
fof(f35328,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v3_lattice3(sK68)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35327,f20899]) ).
fof(f35329,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v3_waybel_3(sK68)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35328,f20898]) ).
fof(f35330,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ l1_orders_2(sK68)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35329,f20897]) ).
fof(f35331,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v1_funct_1(sK69)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35330,f20896]) ).
fof(f35332,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ v1_funct_2(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35331,f20905]) ).
fof(f35333,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,X0))
| ~ r2_hidden(np__0,X0)
| ~ m2_relset_1(sK69,k1_waybel22(sK67),u1_struct_0(sK68))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35332,f20904]) ).
fof(f35334,plain,
! [X0] :
( r2_hidden(k2_yellow_0(sK68,np__0),a_4_0_waybel22(sK67,sK68,sK69,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(sK67)))))) ),
inference(forward_subsumption_resolution,[],[f35333,f20903]) ).
fof(f35335,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))))
| ~ r2_hidden(np__0,X0)
| r2_hidden(k4_yellow_0(sK68),a_4_0_waybel22(sK67,sK68,sK69,X0)) ),
inference(forward_demodulation,[],[f35334,f25486]) ).
fof(f35339,plain,
( ~ r2_hidden(np__0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))))
| r2_hidden(k4_yellow_0(sK68),a_4_0_waybel22(sK67,sK68,sK69,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67)))))))
| ~ l1_orders_2(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))) ),
inference(resolution,[],[f35335,f20925]) ).
fof(f35354,plain,
( ~ r2_hidden(np__0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))))
| r2_hidden(k4_yellow_0(sK68),a_4_0_waybel22(sK67,sK68,sK69,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))))) ),
inference(forward_subsumption_resolution,[],[f35339,f20981]) ).
fof(f35386,plain,
( ~ r2_hidden(np__0,k1_zfmisc_1(sK67))
| r2_hidden(k4_yellow_0(sK68),a_4_0_waybel22(sK67,sK68,sK69,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))))) ),
inference(forward_demodulation,[],[f35354,f24203]) ).
fof(f35388,plain,
r2_hidden(k4_yellow_0(sK68),a_4_0_waybel22(sK67,sK68,sK69,k4_yellow_0(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(sK67))))))),
inference(forward_subsumption_resolution,[],[f35386,f27115]) ).
fof(f35390,plain,
r2_hidden(k4_yellow_0(sK68),a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67))),
inference(forward_demodulation,[],[f35388,f24203]) ).
fof(f37269,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ v2_orders_2(k7_lattice3(sK68))
| ~ v3_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ v3_lattice3(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| v3_struct_0(k7_lattice3(sK68))
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(resolution,[],[f30746,f30213]) ).
fof(f37307,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ v3_orders_2(k7_lattice3(sK68))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ v3_lattice3(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| v3_struct_0(k7_lattice3(sK68))
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37269,f25538]) ).
fof(f37326,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ v4_orders_2(k7_lattice3(sK68))
| ~ v3_lattice3(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| v3_struct_0(k7_lattice3(sK68))
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37307,f25534]) ).
fof(f37342,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ v3_lattice3(k7_lattice3(sK68))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| v3_struct_0(k7_lattice3(sK68))
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37326,f25530]) ).
fof(f37357,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ l1_orders_2(k7_lattice3(sK68))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| v3_struct_0(k7_lattice3(sK68))
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37342,f25526]) ).
fof(f37372,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| v3_struct_0(k7_lattice3(sK68))
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37357,f25518]) ).
fof(f37387,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| ~ m1_subset_1(k2_yellow_0(k7_lattice3(sK68),X0),u1_struct_0(sK68))
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37372,f25542]) ).
fof(f37405,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(k7_lattice3(sK68)))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37387,f26972]) ).
fof(f37411,plain,
( ! [X0] :
( ~ m1_subset_1(k4_yellow_0(sK68),u1_struct_0(sK68))
| ~ r2_hidden(k4_yellow_0(sK68),X0)
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_demodulation,[],[f37405,f25507]) ).
fof(f37413,plain,
( ! [X0] :
( ~ r2_hidden(k4_yellow_0(sK68),X0)
| k4_yellow_0(sK68) = k2_yellow_0(k7_lattice3(sK68),X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37411,f26980]) ).
fof(f37415,plain,
( ! [X0] :
( ~ r2_hidden(k4_yellow_0(sK68),X0)
| k4_yellow_0(sK68) = k1_yellow_0(sK68,X0) )
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_demodulation,[],[f37413,f34596]) ).
fof(f37418,plain,
( k4_yellow_0(sK68) = k1_yellow_0(sK68,a_4_0_waybel22(sK67,sK68,sK69,k1_zfmisc_1(sK67)))
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(resolution,[],[f37415,f35390]) ).
fof(f37428,plain,
( $false
| ~ spl541_13
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(forward_subsumption_resolution,[],[f37418,f30848]) ).
fof(f37429,plain,
( ~ spl541_13
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(avatar_contradiction_clause,[],[f37428]) ).
cnf(s15,plain,
( ~ spl541_12
| spl541_13 ),
inference(sat_conversion,[],[f25479]) ).
cnf(s16,plain,
spl541_12,
inference(sat_conversion,[],[f25482]) ).
cnf(s24,plain,
spl541_14,
inference(sat_conversion,[],[f25579]) ).
cnf(s26,plain,
~ spl541_20,
inference(sat_conversion,[],[f25627]) ).
cnf(s49,plain,
spl541_17,
inference(sat_conversion,[],[f26211]) ).
cnf(s51,plain,
spl541_18,
inference(sat_conversion,[],[f26221]) ).
cnf(s53,plain,
spl541_19,
inference(sat_conversion,[],[f26234]) ).
cnf(s57,plain,
spl541_60,
inference(sat_conversion,[],[f26291]) ).
cnf(s82,plain,
spl541_16,
inference(sat_conversion,[],[f26692]) ).
cnf(s134,plain,
( ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| spl541_143
| ~ spl541_144 ),
inference(sat_conversion,[],[f28014]) ).
cnf(s183,plain,
spl541_180,
inference(sat_conversion,[],[f29869]) ).
cnf(s186,plain,
( spl541_144
| ~ spl541_180 ),
inference(sat_conversion,[],[f29916]) ).
cnf(s297,plain,
( ~ spl541_13
| ~ spl541_14
| ~ spl541_16
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| ~ spl541_60
| ~ spl541_143 ),
inference(sat_conversion,[],[f37429]) ).
cnf(s306,plain,
spl541_144,
inference(rat,[],[s186,s183]) ).
cnf(s310,plain,
( ~ spl541_14
| ~ spl541_17
| ~ spl541_18
| ~ spl541_19
| spl541_20
| spl541_143 ),
inference(rat,[],[s134,s306]) ).
cnf(s325,plain,
spl541_143,
inference(rat,[],[s310,s26,s49,s53,s51,s24]) ).
cnf(s338,plain,
~ spl541_13,
inference(rat,[],[s297,s24,s57,s26,s53,s51,s49,s82,s325]) ).
cnf(s416,plain,
$false,
inference(rat,[],[s15,s338,s16]) ).
fof(f37437,plain,
$false,
inference(avatar_sat_refutation,[],[s416]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT350+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 14:54:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.30/3.89 % (4076289)Detected formulas, will run a generic FOF schedule.
% 14.30/3.89 % (4076302)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1092601993:i=119:av=off:ss=axioms_2990 on theBenchmark for (2990ds/119Mi)
% 14.30/3.89 % (4076300)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=1358155040:i=141695:sd=1:nm=32:gsp=on:ss=included_2990 on theBenchmark for (2990ds/141695Mi)
% 14.30/3.89 % (4076301)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1894277273:i=109:sd=1:ins=1:gsp=on:ss=axioms_2990 on theBenchmark for (2990ds/109Mi)
% 14.30/3.89 % (4076299)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=2343653661:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2990 on theBenchmark for (2990ds/134677Mi)
% 14.30/3.89 % (4076298)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=1130071387:i=141193_2990 on theBenchmark for (2990ds/141193Mi)
% 14.30/3.89 % (4076304)dis-21_1_sil=8000:lcm=predicate:random_seed=2222813793:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/129Mi)
% 14.30/3.89 % (4076303)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1322098742:s2a=on:i=139:gtg=position_2990 on theBenchmark for (2990ds/139Mi)
% 14.30/3.89 % (4076302)Instruction limit reached!
% 14.30/3.89 % (4076302)------------------------------
% 14.30/3.89 % (4076302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.30/3.89 % (4076302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.89 % (4076302)CaDiCaL version: 2.1.3
% 14.30/3.89 % (4076302)Termination reason: Instruction limit
% 14.30/3.89 % (4076302)Termination phase: Preprocessing 2
% 14.30/3.89 % (4076302)Time elapsed: 0.063 s
% 14.30/3.89 % (4076302)Peak memory usage: 112 MB
% 14.30/3.89 % (4076302)Instructions burned: 119 (million)
% 14.30/3.89 % (4076303)Instruction limit reached!
% 14.30/3.89 % (4076303)------------------------------
% 14.30/3.89 % (4076303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.30/3.89 % (4076303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.89 % (4076303)CaDiCaL version: 2.1.3
% 14.30/3.89 % (4076303)Termination reason: Instruction limit
% 14.30/3.89 % (4076303)Termination phase: Property scanning
% 14.30/3.89 % (4076303)Time elapsed: 0.060 s
% 14.30/3.89 % (4076303)Peak memory usage: 109 MB
% 14.30/3.89 % (4076303)Instructions burned: 140 (million)
% 14.30/3.89 % (4076304)Instruction limit reached!
% 14.30/3.89 % (4076304)------------------------------
% 14.30/3.89 % (4076304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.30/3.89 % (4076304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.89 % (4076304)CaDiCaL version: 2.1.3
% 14.30/3.89 % (4076304)Termination reason: Instruction limit
% 14.30/3.89 % (4076304)Termination phase: SInE selection
% 14.30/3.89 % (4076304)Time elapsed: 0.085 s
% 14.30/3.89 % (4076304)Peak memory usage: 109 MB
% 14.30/3.89 % (4076304)Instructions burned: 129 (million)
% 14.30/3.89 % (4076301)Instruction limit reached!
% 14.30/3.89 % (4076301)------------------------------
% 14.30/3.89 % (4076301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.30/3.89 % (4076301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.30/3.89 % (4076301)CaDiCaL version: 2.1.3
% 14.30/3.89 % (4076301)Termination reason: Instruction limit
% 14.30/3.89 % (4076301)Termination phase: Property scanning
% 14.30/3.89 % (4076301)Time elapsed: 0.095 s
% 14.30/3.89 % (4076301)Peak memory usage: 112 MB
% 14.30/3.89 % (4076301)Instructions burned: 110 (million)
% 14.30/3.89 % (4076312)lrs+10_1_sil=8000:sp=occurrence:random_seed=4283331148:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 14.30/3.89 % (4076313)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2941913704:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/157Mi)
% 14.30/3.89 % (4076314)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4226698918:i=325:sd=1:ss=axioms:sgt=32_2987 on theBenchmark for (2987ds/325Mi)
% 14.30/3.89 % (4076312)Instruction limit reached!
% 14.30/3.89 % (4076312)------------------------------
% 14.30/3.89 % (4076312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.30/3.89 % (4076312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.87 % (4076312)CaDiCaL version: 2.1.3
% 21.84/4.87 % (4076312)Termination reason: Instruction limit
% 21.84/4.87 % (4076312)Termination phase: Saturation
% 21.84/4.87 % (4076312)Time elapsed: 0.117 s
% 21.84/4.87 % (4076312)Peak memory usage: 117 MB
% 21.84/4.87 % (4076312)Instructions burned: 287 (million)
% 21.84/4.87 % (4076315)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=3611022441:s2a=on:i=248:s2at=1.23:gtg=position_2987 on theBenchmark for (2987ds/248Mi)
% 21.84/4.87 % (4076313)Instruction limit reached!
% 21.84/4.87 % (4076313)------------------------------
% 21.84/4.87 % (4076313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.84/4.87 % (4076313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.87 % (4076313)CaDiCaL version: 2.1.3
% 21.84/4.87 % (4076313)Termination reason: Instruction limit
% 21.84/4.87 % (4076313)Termination phase: Property scanning
% 21.84/4.87 % (4076313)Time elapsed: 0.068 s
% 21.84/4.87 % (4076313)Peak memory usage: 109 MB
% 21.84/4.87 % (4076313)Instructions burned: 157 (million)
% 21.84/4.87 % (4076315)Instruction limit reached!
% 21.84/4.87 % (4076315)------------------------------
% 21.84/4.87 % (4076315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.84/4.87 % (4076315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.87 % (4076315)CaDiCaL version: 2.1.3
% 21.84/4.87 % (4076315)Termination reason: Instruction limit
% 21.84/4.87 % (4076315)Termination phase: Property scanning
% 21.84/4.87 % (4076315)Time elapsed: 0.106 s
% 21.84/4.87 % (4076315)Peak memory usage: 109 MB
% 21.84/4.87 % (4076315)Instructions burned: 249 (million)
% 21.84/4.87 % (4076320)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4101739119:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2985 on theBenchmark for (2985ds/294Mi)
% 21.84/4.87 % (4076321)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=467148061:i=2350_2985 on theBenchmark for (2985ds/2350Mi)
% 21.84/4.87 % (4076314)Instruction limit reached!
% 21.84/4.87 % (4076314)------------------------------
% 21.84/4.87 % (4076314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.84/4.87 % (4076314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.87 % (4076314)CaDiCaL version: 2.1.3
% 21.84/4.87 % (4076314)Termination reason: Instruction limit
% 21.84/4.87 % (4076314)Termination phase: Saturation
% 21.84/4.87 % (4076314)Time elapsed: 0.228 s
% 21.84/4.87 % (4076314)Peak memory usage: 116 MB
% 21.84/4.87 % (4076314)Instructions burned: 325 (million)
% 21.84/4.87 % (4076320)Instruction limit reached!
% 21.84/4.87 % (4076320)------------------------------
% 21.84/4.87 % (4076320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.84/4.87 % (4076320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.87 % (4076320)CaDiCaL version: 2.1.3
% 21.84/4.87 % (4076320)Termination reason: Instruction limit
% 21.84/4.87 % (4076320)Termination phase: Property scanning
% 21.84/4.87 % (4076320)Time elapsed: 0.130 s
% 21.84/4.87 % (4076320)Peak memory usage: 118 MB
% 21.84/4.87 % (4076320)Instructions burned: 298 (million)
% 21.84/4.87 % (4076322)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1502341058:cts=off:i=113:fsr=off:ss=included:sgt=4_2984 on theBenchmark for (2984ds/113Mi)
% 21.84/4.87 % (4076325)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3942911886:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 21.84/4.87 % (4076322)Instruction limit reached!
% 21.84/4.87 % (4076322)------------------------------
% 21.84/4.87 % (4076322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.84/4.87 % (4076322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.84/4.87 % (4076322)CaDiCaL version: 2.1.3
% 21.84/4.87 % (4076322)Termination reason: Instruction limit
% 21.84/4.87 % (4076322)Termination phase: Preprocessing 1
% 21.84/4.87 % (4076322)Time elapsed: 0.098 s
% 21.84/4.87 % (4076322)Peak memory usage: 110 MB
% 21.84/4.87 % (4076322)Instructions burned: 113 (million)
% 21.84/4.87 % (4076326)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2334842478:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2983 on theBenchmark for (2983ds/114Mi)
% 21.84/4.87 % (4076326)Instruction limit reached!
% 21.84/4.87 % (4076326)------------------------------
% 21.84/4.87 % (4076326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/10.45 % (4076326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/10.45 % (4076326)CaDiCaL version: 2.1.3
% 62.14/10.45 % (4076326)Termination reason: Instruction limit
% 62.14/10.45 % (4076326)Termination phase: Property scanning
% 62.14/10.45 % (4076326)Time elapsed: 0.027 s
% 62.14/10.45 % (4076326)Peak memory usage: 109 MB
% 62.14/10.45 % (4076326)Instructions burned: 116 (million)
% 62.14/10.45 % (4076325)Instruction limit reached!
% 62.14/10.45 % (4076325)------------------------------
% 62.14/10.45 % (4076325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/10.45 % (4076325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/10.45 % (4076325)CaDiCaL version: 2.1.3
% 62.14/10.45 % (4076325)Termination reason: Instruction limit
% 62.14/10.45 % (4076325)Termination phase: Preprocessing 1
% 62.14/10.45 % (4076325)Time elapsed: 0.091 s
% 62.14/10.45 % (4076325)Peak memory usage: 110 MB
% 62.14/10.45 % (4076325)Instructions burned: 128 (million)
% 62.14/10.45 % (4076329)lrs+10_1_sil=8000:sp=occurrence:random_seed=861236289:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2982 on theBenchmark for (2982ds/907Mi)
% 62.14/10.45 % (4076331)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2248115999:i=437:sd=1:aac=none:ss=included_2981 on theBenchmark for (2981ds/437Mi)
% 62.14/10.45 % (4076331)Refutation not found, incomplete strategy
% 62.14/10.45 % (4076331)------------------------------
% 62.14/10.45 % (4076331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/10.45 % (4076331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/10.45 % (4076331)CaDiCaL version: 2.1.3
% 62.14/10.45 % (4076331)Termination reason: Refutation not found, incomplete strategy
% 62.14/10.45 % (4076331)Time elapsed: 0.076 s
% 62.14/10.45 % (4076331)Peak memory usage: 116 MB
% 62.14/10.45 % (4076331)Instructions burned: 168 (million)
% 62.14/10.45 % (4076332)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3038036511:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 62.14/10.45 % (4076331)------------------------------
% 62.14/10.45 % (4076331)------------------------------
% 62.14/10.45 % (4076336)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2572197730:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 62.14/10.45 % (4076329)Instruction limit reached!
% 62.14/10.45 % (4076329)------------------------------
% 62.14/10.45 % (4076329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/10.45 % (4076329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/10.45 % (4076329)CaDiCaL version: 2.1.3
% 62.14/10.45 % (4076329)Termination reason: Instruction limit
% 62.14/10.45 % (4076329)Termination phase: Saturation
% 62.14/10.45 % (4076329)Time elapsed: 0.521 s
% 62.14/10.45 % (4076329)Peak memory usage: 128 MB
% 62.14/10.45 % (4076329)Instructions burned: 909 (million)
% 62.14/10.45 % (4076336)Instruction limit reached!
% 62.14/10.45 % (4076336)------------------------------
% 62.14/10.45 % (4076336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/10.45 % (4076336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/10.45 % (4076336)CaDiCaL version: 2.1.3
% 62.14/10.45 % (4076336)Termination reason: Instruction limit
% 62.14/10.45 % (4076336)Termination phase: NewCNF
% 62.14/10.45 % (4076336)Time elapsed: 0.120 s
% 62.14/10.45 % (4076336)Peak memory usage: 113 MB
% 62.14/10.45 % (4076336)Instructions burned: 135 (million)
% 62.14/10.45 % (4076338)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4177106464:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 62.14/10.45 % (4076339)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1964089850:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 62.14/10.45 % (4076321)Instruction limit reached!
% 62.14/10.45 % (4076321)------------------------------
% 62.14/10.45 % (4076321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.14/10.45 % (4076321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.14/10.45 % (4076321)CaDiCaL version: 2.1.3
% 62.14/10.45 % (4076321)Termination reason: Instruction limit
% 62.14/10.45 % (4076321)Termination phase: Saturation
% 62.14/10.45 % (4076321)Time elapsed: 1.245 s
% 62.14/10.45 % (4076321)Peak memory usage: 174 MB
% 62.14/10.45 % (4076321)Instructions burned: 2351 (million)
% 62.14/10.45 % (4076342)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=1011177831:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/125Mi)
% 89.84/14.35 % (4076338)Instruction limit reached!
% 89.84/14.35 % (4076338)------------------------------
% 89.84/14.35 % (4076338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.84/14.35 % (4076338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.84/14.35 % (4076338)CaDiCaL version: 2.1.3
% 89.84/14.35 % (4076338)Termination reason: Instruction limit
% 89.84/14.35 % (4076338)Termination phase: Preprocessing 3
% 89.84/14.35 % (4076338)Time elapsed: 0.432 s
% 89.84/14.35 % (4076338)Peak memory usage: 132 MB
% 89.84/14.35 % (4076338)Instructions burned: 593 (million)
% 89.84/14.35 % (4076342)Instruction limit reached!
% 89.84/14.35 % (4076342)------------------------------
% 89.84/14.35 % (4076342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.84/14.35 % (4076342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.84/14.35 % (4076342)CaDiCaL version: 2.1.3
% 89.84/14.35 % (4076342)Termination reason: Instruction limit
% 89.84/14.35 % (4076342)Termination phase: Property scanning
% 89.84/14.35 % (4076342)Time elapsed: 0.056 s
% 89.84/14.35 % (4076342)Peak memory usage: 110 MB
% 89.84/14.35 % (4076342)Instructions burned: 127 (million)
% 89.84/14.35 % (4076344)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=198531127:i=134:gtgl=5:slsql=off:gtg=exists_sym_2969 on theBenchmark for (2969ds/134Mi)
% 89.84/14.35 % (4076345)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2839191384:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/141Mi)
% 89.84/14.35 % (4076344)Instruction limit reached!
% 89.84/14.35 % (4076344)------------------------------
% 89.84/14.35 % (4076344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.84/14.35 % (4076344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.84/14.35 % (4076344)CaDiCaL version: 2.1.3
% 89.84/14.35 % (4076344)Termination reason: Instruction limit
% 89.84/14.35 % (4076344)Termination phase: Property scanning
% 89.84/14.35 % (4076344)Time elapsed: 0.058 s
% 89.84/14.35 % (4076344)Peak memory usage: 109 MB
% 89.84/14.35 % (4076344)Instructions burned: 135 (million)
% 89.84/14.35 % (4076345)Refutation not found, incomplete strategy
% 89.84/14.35 % (4076345)------------------------------
% 89.84/14.35 % (4076345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.84/14.35 % (4076345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.84/14.35 % (4076345)CaDiCaL version: 2.1.3
% 89.84/14.35 % (4076345)Termination reason: Refutation not found, incomplete strategy
% 89.84/14.35 % (4076345)Time elapsed: 0.101 s
% 89.84/14.35 % (4076345)Peak memory usage: 115 MB
% 89.84/14.35 % (4076345)Instructions burned: 118 (million)
% 89.84/14.35 % (4076348)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1129937593:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2967 on theBenchmark for (2967ds/431Mi)
% 89.84/14.35 % (4076345)------------------------------
% 89.84/14.35 % (4076345)------------------------------
% 89.84/14.35 % (4076348)Instruction limit reached!
% 89.84/14.35 % (4076348)------------------------------
% 89.84/14.35 % (4076348)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.84/14.35 % (4076348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.84/14.35 % (4076348)CaDiCaL version: 2.1.3
% 89.84/14.35 % (4076348)Termination reason: Instruction limit
% 89.84/14.35 % (4076348)Termination phase: Saturation
% 89.84/14.35 % (4076348)Time elapsed: 0.286 s
% 89.84/14.35 % (4076348)Peak memory usage: 117 MB
% 89.84/14.35 % (4076348)Instructions burned: 433 (million)
% 89.84/14.35 % (4076350)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=2726322368:i=6060:aac=none:ins=25_2963 on theBenchmark for (2963ds/6060Mi)
% 89.84/14.35 % (4076351)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=1250958761:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2962 on theBenchmark for (2962ds/150Mi)
% 89.84/14.35 % (4076351)Instruction limit reached!
% 89.84/14.35 % (4076351)------------------------------
% 89.84/14.35 % (4076351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.84/14.35 % (4076351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.51 % (4076351)CaDiCaL version: 2.1.3
% 64.87/16.51 % (4076351)Termination reason: Instruction limit
% 64.87/16.51 % (4076351)Termination phase: Preprocessing 1
% 64.87/16.51 % (4076351)Time elapsed: 0.121 s
% 64.87/16.51 % (4076351)Peak memory usage: 111 MB
% 64.87/16.51 % (4076351)Instructions burned: 151 (million)
% 64.87/16.51 % (4076354)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3283562266:i=14155:bd=all_2959 on theBenchmark for (2959ds/14155Mi)
% 64.87/16.51 % (4076332)Instruction limit reached!
% 64.87/16.51 % (4076332)------------------------------
% 64.87/16.51 % (4076332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.51 % (4076332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.51 % (4076332)CaDiCaL version: 2.1.3
% 64.87/16.51 % (4076332)Termination reason: Instruction limit
% 64.87/16.51 % (4076332)Termination phase: Saturation
% 64.87/16.51 % (4076332)Time elapsed: 3.247 s
% 64.87/16.51 % (4076332)Peak memory usage: 205 MB
% 64.87/16.51 % (4076332)Instructions burned: 5202 (million)
% 64.87/16.51 % (4076356)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2952256350:i=667:av=off:fsr=off_2947 on theBenchmark for (2947ds/667Mi)
% 64.87/16.51 % (4076356)Instruction limit reached!
% 64.87/16.51 % (4076356)------------------------------
% 64.87/16.51 % (4076356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.51 % (4076356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.51 % (4076356)CaDiCaL version: 2.1.3
% 64.87/16.51 % (4076356)Termination reason: Instruction limit
% 64.87/16.51 % (4076356)Termination phase: NewCNF
% 64.87/16.51 % (4076356)Time elapsed: 0.504 s
% 64.87/16.51 % (4076356)Peak memory usage: 145 MB
% 64.87/16.51 % (4076356)Instructions burned: 668 (million)
% 64.87/16.51 % (4076358)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=2471891339:s2a=on:i=185:s2at=1.8:fdi=4_2940 on theBenchmark for (2940ds/185Mi)
% 64.87/16.51 % (4076358)Instruction limit reached!
% 64.87/16.51 % (4076358)------------------------------
% 64.87/16.51 % (4076358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.51 % (4076358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.51 % (4076358)CaDiCaL version: 2.1.3
% 64.87/16.51 % (4076358)Termination reason: Instruction limit
% 64.87/16.51 % (4076358)Termination phase: SInE selection
% 64.87/16.51 % (4076358)Time elapsed: 0.156 s
% 64.87/16.51 % (4076358)Peak memory usage: 110 MB
% 64.87/16.51 % (4076358)Instructions burned: 185 (million)
% 64.87/16.51 % (4076360)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=864911847:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2937 on theBenchmark for (2937ds/193Mi)
% 64.87/16.51 % (4076360)Instruction limit reached!
% 64.87/16.51 % (4076360)------------------------------
% 64.87/16.51 % (4076360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.51 % (4076360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.51 % (4076360)CaDiCaL version: 2.1.3
% 64.87/16.51 % (4076360)Termination reason: Instruction limit
% 64.87/16.51 % (4076360)Termination phase: SInE selection
% 64.87/16.51 % (4076360)Time elapsed: 0.156 s
% 64.87/16.52 % (4076360)Peak memory usage: 109 MB
% 64.87/16.52 % (4076360)Instructions burned: 194 (million)
% 64.87/16.52 % (4076362)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1696530896:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2933 on theBenchmark for (2933ds/4850Mi)
% 64.87/16.52 % (4076350)Instruction limit reached!
% 64.87/16.52 % (4076350)------------------------------
% 64.87/16.52 % (4076350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076350)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076350)Termination reason: Instruction limit
% 64.87/16.52 % (4076350)Termination phase: Saturation
% 64.87/16.52 % (4076350)Time elapsed: 4.684 s
% 64.87/16.52 % (4076350)Peak memory usage: 574 MB
% 64.87/16.52 % (4076350)Instructions burned: 6060 (million)
% 64.87/16.52 % (4076364)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=801605628:i=12111:sd=1:ss=included_2914 on theBenchmark for (2914ds/12111Mi)
% 64.87/16.52 % (4076362)Instruction limit reached!
% 64.87/16.52 % (4076362)------------------------------
% 64.87/16.52 % (4076362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076362)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076362)Termination reason: Instruction limit
% 64.87/16.52 % (4076362)Termination phase: Saturation
% 64.87/16.52 % (4076362)Time elapsed: 2.790 s
% 64.87/16.52 % (4076362)Peak memory usage: 205 MB
% 64.87/16.52 % (4076362)Instructions burned: 4851 (million)
% 64.87/16.52 % (4076366)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=819174978:i=319:kws=precedence:fsr=off_2903 on theBenchmark for (2903ds/319Mi)
% 64.87/16.52 % (4076366)Instruction limit reached!
% 64.87/16.52 % (4076366)------------------------------
% 64.87/16.52 % (4076366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076366)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076366)Termination reason: Instruction limit
% 64.87/16.52 % (4076366)Termination phase: Naming
% 64.87/16.52 % (4076366)Time elapsed: 0.244 s
% 64.87/16.52 % (4076366)Peak memory usage: 131 MB
% 64.87/16.52 % (4076366)Instructions burned: 320 (million)
% 64.87/16.52 % (4076368)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=605062349:i=2064:ep=RST_2899 on theBenchmark for (2899ds/2064Mi)
% 64.87/16.52 % (4076339)Instruction limit reached!
% 64.87/16.52 % (4076339)------------------------------
% 64.87/16.52 % (4076339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076339)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076339)Termination reason: Instruction limit
% 64.87/16.52 % (4076339)Termination phase: Saturation
% 64.87/16.52 % (4076339)Time elapsed: 7.670 s
% 64.87/16.52 % (4076339)Peak memory usage: 303 MB
% 64.87/16.52 % (4076339)Instructions burned: 13194 (million)
% 64.87/16.52 % (4076370)dis-1011_128_sil=32000:random_seed=150212113:i=3706:ep=RST:av=off_2896 on theBenchmark for (2896ds/3706Mi)
% 64.87/16.52 % (4076368)Instruction limit reached!
% 64.87/16.52 % (4076368)------------------------------
% 64.87/16.52 % (4076368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076368)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076368)Termination reason: Instruction limit
% 64.87/16.52 % (4076368)Termination phase: Property scanning
% 64.87/16.52 % (4076368)Time elapsed: 1.041 s
% 64.87/16.52 % (4076368)Peak memory usage: 162 MB
% 64.87/16.52 % (4076368)Instructions burned: 2066 (million)
% 64.87/16.52 % (4076372)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3263063831:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2887 on theBenchmark for (2887ds/757Mi)
% 64.87/16.52 % (4076372)Instruction limit reached!
% 64.87/16.52 % (4076372)------------------------------
% 64.87/16.52 % (4076372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076372)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076372)Termination reason: Instruction limit
% 64.87/16.52 % (4076372)Termination phase: Saturation
% 64.87/16.52 % (4076372)Time elapsed: 0.514 s
% 64.87/16.52 % (4076372)Peak memory usage: 127 MB
% 64.87/16.52 % (4076372)Instructions burned: 757 (million)
% 64.87/16.52 % (4076374)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2557747763:i=13913:ss=axioms:sgt=8_2880 on theBenchmark for (2880ds/13913Mi)
% 64.87/16.52 % (4076370)Instruction limit reached!
% 64.87/16.52 % (4076370)------------------------------
% 64.87/16.52 % (4076370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076370)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076370)Termination reason: Instruction limit
% 64.87/16.52 % (4076370)Termination phase: Saturation
% 64.87/16.52 % (4076370)Time elapsed: 1.902 s
% 64.87/16.52 % (4076370)Peak memory usage: 180 MB
% 64.87/16.52 % (4076370)Instructions burned: 3706 (million)
% 64.87/16.52 % (4076376)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=903890687:i=9925:aac=none_2875 on theBenchmark for (2875ds/9925Mi)
% 64.87/16.52 % (4076354)Instruction limit reached!
% 64.87/16.52 % (4076354)------------------------------
% 64.87/16.52 % (4076354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076354)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076354)Termination reason: Instruction limit
% 64.87/16.52 % (4076354)Termination phase: Saturation
% 64.87/16.52 % (4076354)Time elapsed: 9.309 s
% 64.87/16.52 % (4076354)Peak memory usage: 663 MB
% 64.87/16.52 % (4076354)Instructions burned: 14156 (million)
% 64.87/16.52 % (4076378)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3285023431:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2864 on theBenchmark for (2864ds/2479Mi)
% 64.87/16.52 % (4076378)Instruction limit reached!
% 64.87/16.52 % (4076378)------------------------------
% 64.87/16.52 % (4076378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.87/16.52 % (4076378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.87/16.52 % (4076378)CaDiCaL version: 2.1.3
% 64.87/16.52 % (4076378)Termination reason: Instruction limit
% 64.87/16.52 % (4076378)Termination phase: Saturation
% 64.87/16.52 % (4076378)Time elapsed: 1.481 s
% 64.87/16.52 % (4076378)Peak memory usage: 131 MB
% 64.87/16.52 % (4076378)Instructions burned: 2479 (million)
% 64.87/16.52 % (4076374)First to succeed.
% 64.87/16.52 % (4076374)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4076289"
% 64.87/16.52 % (4076380)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=235819687:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2847 on theBenchmark for (2847ds/440Mi)
% 64.87/16.52 % (4076374)Refutation found. Thanks to Tanya!
% 64.87/16.52 % SZS status Theorem for theBenchmark
% 64.87/16.52 % SZS output start Proof for theBenchmark
% See solution above
% 105.46/16.73 % (4076374)------------------------------
% 105.46/16.73 % (4076374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.46/16.73 % (4076374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.46/16.73 % (4076374)CaDiCaL version: 2.1.3
% 105.46/16.73 % (4076374)Termination reason: Refutation
% 105.46/16.73 % (4076374)Time elapsed: 3.205 s
% 105.46/16.73 % (4076374)Peak memory usage: 200 MB
% 105.46/16.73 % (4076374)Instructions burned: 5013 (million)
% 105.46/16.73 % (4076374)------------------------------
% 105.46/16.73 % (4076374)------------------------------
% 105.46/16.73 % (4076289)Success in time 15.663 s
% 105.46/16.73 % Vampire exiting
%------------------------------------------------------------------------------