%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT350+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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 25.96s 4.45s
% Output : Refutation 26.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 46
% Syntax : Number of formulae : 424 ( 83 unt; 17 def)
% Number of atoms : 2433 ( 183 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 3577 (1568 ~;1608 |; 335 &)
% ( 29 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 43 ( 41 usr; 9 prp; 0-3 aty)
% Number of functors : 38 ( 38 usr; 13 con; 0-5 aty)
% Number of variables : 557 ( 0 sgn 527 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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/sandbox/benchmark/theBenchmark.p',t13_waybel22) ).
fof(f2,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)],[f1]) ).
fof(f5,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/sandbox/benchmark/theBenchmark.p',cc10_waybel_0) ).
fof(f16,axiom,
! [X0] :
( l1_orders_2(X0)
=> ( ( ~ v3_struct_0(X0)
& v3_lattice3(X0) )
=> ( ~ v3_struct_0(X0)
& v1_lattice3(X0)
& v2_lattice3(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_yellow_0) ).
fof(f31,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/sandbox/benchmark/theBenchmark.p',cc9_waybel_0) ).
fof(f32,axiom,
! [X0] :
( l1_orders_2(X0)
=> k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_yellow_0) ).
fof(f34,axiom,
! [X0] :
( X0 = k1_xboole_0
<=> ! [X1] : ~ r2_hidden(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f35,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_orders_2(X0)
& v3_orders_2(X0)
& l1_orders_2(X0) )
=> k9_waybel_0(X0) = a_1_1_waybel_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d24_waybel_0) ).
fof(f36,axiom,
! [X0] : k1_waybel22(X0) = a_1_0_waybel22(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_waybel22) ).
fof(f37,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/sandbox/benchmark/theBenchmark.p',d3_waybel22) ).
fof(f38,axiom,
! [X0] :
( l1_orders_2(X0)
=> ! [X1,X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( r2_lattice3(X0,X1,X2)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r2_hidden(X3,X1)
=> r1_orders_2(X0,X3,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d9_lattice3) ).
fof(f46,axiom,
! [X0,X1] :
( l1_orders_2(X0)
=> m1_subset_1(k1_yellow_0(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f48,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/sandbox/benchmark/theBenchmark.p',dt_k2_waybel22) ).
fof(f49,axiom,
! [X0,X1] :
( l1_orders_2(X0)
=> m1_subset_1(k2_yellow_0(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_0) ).
fof(f50,axiom,
! [X0] :
( v1_orders_2(k2_yellow_1(X0))
& l1_orders_2(k2_yellow_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_yellow_1) ).
fof(f52,axiom,
! [X0] :
( v1_orders_2(k3_yellow_1(X0))
& l1_orders_2(k3_yellow_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k3_yellow_1) ).
fof(f53,axiom,
! [X0] :
( l1_orders_2(X0)
=> m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_yellow_0) ).
fof(f75,axiom,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v2_waybel_1(k3_yellow_1(X0))
& v9_waybel_1(k3_yellow_1(X0))
& v10_waybel_1(k3_yellow_1(X0))
& v11_waybel_1(k3_yellow_1(X0))
& v2_waybel_3(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v1_waybel_8(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc14_waybel_8) ).
fof(f78,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f96,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/sandbox/benchmark/theBenchmark.p',fraenkel_a_4_0_waybel22) ).
fof(f97,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/sandbox/benchmark/theBenchmark.p',fraenkel_a_4_1_waybel22) ).
fof(f120,axiom,
! [X0,X1,X2] :
( m2_relset_1(X2,X0,X1)
<=> m1_relset_1(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f121,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/sandbox/benchmark/theBenchmark.p',redefinition_r3_orders_2) ).
fof(f124,axiom,
! [X0] : k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))) = k1_zfmisc_1(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_waybel16) ).
fof(f125,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f126,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f128,axiom,
! [X0] : r1_tarski(k1_xboole_0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_xboole_1) ).
fof(f129,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_orders_2(X0)
& v3_lattice3(X0)
& l1_orders_2(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( X1 = k1_yellow_0(X0,X2)
<=> ( r2_lattice3(X0,X2,X1)
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r2_lattice3(X0,X2,X3)
=> r1_orders_2(X0,X1,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t32_yellow_0) ).
fof(f130,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f133,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,k4_yellow_0(X0),X1)
=> X1 = k4_yellow_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_waybel15) ).
fof(f138,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
=> m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(unused_predicate_definition_removal,[],[f130]) ).
fof(f139,plain,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v2_waybel_1(k3_yellow_1(X0))
& v9_waybel_1(k3_yellow_1(X0))
& v10_waybel_1(k3_yellow_1(X0))
& v2_waybel_3(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v1_waybel_8(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
inference(pure_predicate_removal,[],[f75]) ).
fof(f140,plain,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v2_waybel_1(k3_yellow_1(X0))
& v9_waybel_1(k3_yellow_1(X0))
& v2_waybel_3(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v1_waybel_8(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
inference(pure_predicate_removal,[],[f139]) ).
fof(f142,plain,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v9_waybel_1(k3_yellow_1(X0))
& v2_waybel_3(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v1_waybel_8(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
inference(pure_predicate_removal,[],[f140]) ).
fof(f148,plain,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v2_waybel_3(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v1_waybel_8(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
inference(pure_predicate_removal,[],[f142]) ).
fof(f149,plain,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v2_waybel_3(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
inference(pure_predicate_removal,[],[f148]) ).
fof(f158,plain,
! [X0] :
( ~ v3_struct_0(k3_yellow_1(X0))
& v1_orders_2(k3_yellow_1(X0))
& v2_orders_2(k3_yellow_1(X0))
& v3_orders_2(k3_yellow_1(X0))
& v4_orders_2(k3_yellow_1(X0))
& v1_lattice3(k3_yellow_1(X0))
& v2_lattice3(k3_yellow_1(X0))
& v3_lattice3(k3_yellow_1(X0))
& v1_yellow_0(k3_yellow_1(X0))
& v2_yellow_0(k3_yellow_1(X0))
& v3_yellow_0(k3_yellow_1(X0))
& v24_waybel_0(k3_yellow_1(X0))
& v25_waybel_0(k3_yellow_1(X0))
& v3_waybel_3(k3_yellow_1(X0))
& v2_waybel_8(k3_yellow_1(X0)) ),
inference(pure_predicate_removal,[],[f149]) ).
fof(f163,plain,
? [X0,X1] :
( ? [X2] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) != k4_yellow_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f164,plain,
? [X0,X1] :
( ? [X2] :
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))) != k4_yellow_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k1_waybel22(X0),u1_struct_0(X1))
& m2_relset_1(X2,k1_waybel22(X0),u1_struct_0(X1)) )
& ~ v3_struct_0(X1)
& v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v3_lattice3(X1)
& v3_waybel_3(X1)
& l1_orders_2(X1) ),
inference(flattening,[],[f163]) ).
fof(f168,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,[],[f5]) ).
fof(f169,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,[],[f168]) ).
fof(f188,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_lattice3(X0)
& v2_lattice3(X0) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f189,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v1_lattice3(X0)
& v2_lattice3(X0) )
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f188]) ).
fof(f218,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,[],[f31]) ).
fof(f219,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,[],[f218]) ).
fof(f220,plain,
! [X0] :
( k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f223,plain,
! [X0] :
( k9_waybel_0(X0) = a_1_1_waybel_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f35]) ).
fof(f224,plain,
! [X0] :
( k9_waybel_0(X0) = a_1_1_waybel_0(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f223]) ).
fof(f225,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,[],[f37]) ).
fof(f226,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,[],[f225]) ).
fof(f227,plain,
! [X0] :
( ! [X1,X2] :
( ( r2_lattice3(X0,X1,X2)
<=> ! [X3] :
( r1_orders_2(X0,X3,X2)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f228,plain,
! [X0] :
( ! [X1,X2] :
( ( r2_lattice3(X0,X1,X2)
<=> ! [X3] :
( r1_orders_2(X0,X3,X2)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f227]) ).
fof(f234,plain,
! [X0,X1] :
( m1_subset_1(k1_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f235,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,[],[f48]) ).
fof(f236,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,[],[f235]) ).
fof(f237,plain,
! [X0,X1] :
( m1_subset_1(k2_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f238,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f53]) ).
fof(f288,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,[],[f96]) ).
fof(f289,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,[],[f288]) ).
fof(f290,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,[],[f97]) ).
fof(f291,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,[],[f290]) ).
fof(f302,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,[],[f121]) ).
fof(f303,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,[],[f302]) ).
fof(f306,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f125]) ).
fof(f307,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f126]) ).
fof(f308,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f307]) ).
fof(f310,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = k1_yellow_0(X0,X2)
<=> ( r2_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X1,X3)
| ~ r2_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(ennf_transformation,[],[f129]) ).
fof(f311,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = k1_yellow_0(X0,X2)
<=> ( r2_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X1,X3)
| ~ r2_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f310]) ).
fof(f312,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(ennf_transformation,[],[f138]) ).
fof(f316,plain,
! [X0] :
( ! [X1] :
( X1 = k4_yellow_0(X0)
| ~ r1_orders_2(X0,k4_yellow_0(X0),X1)
| ~ 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,[],[f133]) ).
fof(f317,plain,
! [X0] :
( ! [X1] :
( X1 = k4_yellow_0(X0)
| ~ r1_orders_2(X0,k4_yellow_0(X0),X1)
| ~ 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,[],[f316]) ).
fof(f337,plain,
( k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,k2_waybel22(sK8,sK9,sK10),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) != k4_yellow_0(sK9)
& v1_funct_1(sK10)
& v1_funct_2(sK10,k1_waybel22(sK8),u1_struct_0(sK9))
& m2_relset_1(sK10,k1_waybel22(sK8),u1_struct_0(sK9))
& ~ v3_struct_0(sK9)
& v2_orders_2(sK9)
& v3_orders_2(sK9)
& v4_orders_2(sK9)
& v3_lattice3(sK9)
& v3_waybel_3(sK9)
& l1_orders_2(sK9) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10)],[f164]) ).
fof(f343,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X1] : ~ r2_hidden(X1,X0)
| k1_xboole_0 != X0 ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f344,plain,
! [X0] :
( ( X0 = k1_xboole_0
| ? [X1] : r2_hidden(X1,X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(rectify,[],[f343]) ).
fof(f345,plain,
! [X0] :
( ( X0 = k1_xboole_0
| r2_hidden(sK11(X0),X0) )
& ( ! [X2] : ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X1,sK11(X0))],[f344]) ).
fof(f346,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,[],[f226]) ).
fof(f347,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,[],[f346]) ).
fof(f348,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,sK12(X0,X1,X2,X3)) != k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,sK12(X0,X1,X2,X3)))
& m1_subset_1(sK12(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,[sK12]),skolemize(X4,sK12(X0,X1,X2,X3))],[f347]) ).
fof(f349,plain,
! [X0] :
( ! [X1,X2] :
( ( ( r2_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r1_orders_2(X0,X3,X2)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X3] :
( r1_orders_2(X0,X3,X2)
| ~ r2_hidden(X3,X1)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ r2_lattice3(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f228]) ).
fof(f350,plain,
! [X0] :
( ! [X1,X2] :
( ( ( r2_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r1_orders_2(X0,X3,X2)
& r2_hidden(X3,X1)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X4] :
( r1_orders_2(X0,X4,X2)
| ~ r2_hidden(X4,X1)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ r2_lattice3(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f349]) ).
fof(f351,plain,
! [X0] :
( ! [X1,X2] :
( ( ( r2_lattice3(X0,X1,X2)
| ( ~ r1_orders_2(X0,sK13(X0,X1,X2),X2)
& r2_hidden(sK13(X0,X1,X2),X1)
& m1_subset_1(sK13(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ! [X4] :
( r1_orders_2(X0,X4,X2)
| ~ r2_hidden(X4,X1)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ r2_lattice3(X0,X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X3,sK13(X0,X1,X2))],[f350]) ).
fof(f366,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,[],[f289]) ).
fof(f367,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,[],[f366]) ).
fof(f368,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(sK22(X0,X1,X2,X3,X4),k1_zfmisc_1(X1))
& k2_yellow_0(X2,a_4_1_waybel22(X1,X2,X3,sK22(X0,X1,X2,X3,X4))) = X0
& r2_hidden(sK22(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,[sK22]),skolemize(X6,sK22(X0,X1,X2,X3,X4))],[f367]) ).
fof(f369,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,[],[f291]) ).
fof(f370,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,[],[f369]) ).
fof(f371,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(sK23(X0,X1,X3,X4),u1_struct_0(k3_yellow_1(X1)))
& k1_funct_1(X3,k7_waybel_0(k3_yellow_1(X1),sK23(X0,X1,X3,X4))) = X0
& m1_subset_1(sK24(X0,X1,X3,X4),X1)
& sK23(X0,X1,X3,X4) = k1_tarski(sK24(X0,X1,X3,X4))
& r2_hidden(sK24(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,[sK23,sK24]),skolemize(X7,sK23(X0,X1,X3,X4)),skolemize(X8,sK24(X0,X1,X3,X4))],[f370]) ).
fof(f391,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,[],[f120]) ).
fof(f392,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,[],[f303]) ).
fof(f395,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k1_yellow_0(X0,X2)
| ~ r2_lattice3(X0,X2,X1)
| ? [X3] :
( ~ r1_orders_2(X0,X1,X3)
& r2_lattice3(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r2_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X1,X3)
| ~ r2_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k1_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(nnf_transformation,[],[f311]) ).
fof(f396,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k1_yellow_0(X0,X2)
| ~ r2_lattice3(X0,X2,X1)
| ? [X3] :
( ~ r1_orders_2(X0,X1,X3)
& r2_lattice3(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r2_lattice3(X0,X2,X1)
& ! [X3] :
( r1_orders_2(X0,X1,X3)
| ~ r2_lattice3(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k1_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(flattening,[],[f395]) ).
fof(f397,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k1_yellow_0(X0,X2)
| ~ r2_lattice3(X0,X2,X1)
| ? [X3] :
( ~ r1_orders_2(X0,X1,X3)
& r2_lattice3(X0,X2,X3)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r2_lattice3(X0,X2,X1)
& ! [X4] :
( r1_orders_2(X0,X1,X4)
| ~ r2_lattice3(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k1_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(rectify,[],[f396]) ).
fof(f398,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k1_yellow_0(X0,X2)
| ~ r2_lattice3(X0,X2,X1)
| ( ~ r1_orders_2(X0,X1,sK45(X0,X1,X2))
& r2_lattice3(X0,X2,sK45(X0,X1,X2))
& m1_subset_1(sK45(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ( r2_lattice3(X0,X2,X1)
& ! [X4] :
( r1_orders_2(X0,X1,X4)
| ~ r2_lattice3(X0,X2,X4)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k1_yellow_0(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(X3,sK45(X0,X1,X2))],[f397]) ).
fof(f399,plain,
l1_orders_2(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f400,plain,
v3_waybel_3(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f401,plain,
v3_lattice3(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f402,plain,
v4_orders_2(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f403,plain,
v3_orders_2(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f404,plain,
v2_orders_2(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f405,plain,
~ v3_struct_0(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f406,plain,
m2_relset_1(sK10,k1_waybel22(sK8),u1_struct_0(sK9)),
inference(cnf_transformation,[],[f337]) ).
fof(f407,plain,
v1_funct_2(sK10,k1_waybel22(sK8),u1_struct_0(sK9)),
inference(cnf_transformation,[],[f337]) ).
fof(f408,plain,
v1_funct_1(sK10),
inference(cnf_transformation,[],[f337]) ).
fof(f409,plain,
k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,k2_waybel22(sK8,sK9,sK10),k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) != k4_yellow_0(sK9),
inference(cnf_transformation,[],[f337]) ).
fof(f413,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_lattice3(X0)
| v24_waybel_0(X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f455,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v3_lattice3(X0)
| v1_lattice3(X0) ),
inference(cnf_transformation,[],[f189]) ).
fof(f530,plain,
! [X0] :
( ~ v1_lattice3(X0)
| ~ v2_orders_2(X0)
| v2_yellow_0(X0)
| ~ v24_waybel_0(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f219]) ).
fof(f534,plain,
! [X0] :
( ~ l1_orders_2(X0)
| k4_yellow_0(X0) = k2_yellow_0(X0,k1_xboole_0) ),
inference(cnf_transformation,[],[f220]) ).
fof(f536,plain,
! [X2,X0] :
( ~ r2_hidden(X2,X0)
| k1_xboole_0 != X0 ),
inference(cnf_transformation,[],[f345]) ).
fof(f537,plain,
! [X0] :
( r2_hidden(sK11(X0),X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f345]) ).
fof(f538,plain,
! [X0] :
( ~ l1_orders_2(X0)
| v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| k9_waybel_0(X0) = a_1_1_waybel_0(X0) ),
inference(cnf_transformation,[],[f224]) ).
fof(f539,plain,
! [X0] : k1_waybel22(X0) = a_1_0_waybel22(X0),
inference(cnf_transformation,[],[f36]) ).
fof(f540,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,[],[f348]) ).
fof(f543,plain,
! [X2,X0,X1,X4] :
( ~ r2_lattice3(X0,X1,X2)
| ~ r2_hidden(X4,X1)
| ~ m1_subset_1(X4,u1_struct_0(X0))
| r1_orders_2(X0,X4,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f351]) ).
fof(f552,plain,
! [X0,X1] :
( m1_subset_1(k1_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f234]) ).
fof(f553,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,[],[f236]) ).
fof(f554,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,[],[f236]) ).
fof(f555,plain,
! [X2,X0,X1] :
( v1_funct_1(k2_waybel22(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)) ),
inference(cnf_transformation,[],[f236]) ).
fof(f556,plain,
! [X0,X1] :
( m1_subset_1(k2_yellow_0(X0,X1),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f557,plain,
! [X0] : l1_orders_2(k2_yellow_1(X0)),
inference(cnf_transformation,[],[f50]) ).
fof(f559,plain,
! [X0] : l1_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f52]) ).
fof(f561,plain,
! [X0] :
( m1_subset_1(k4_yellow_0(X0),u1_struct_0(X0))
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f238]) ).
fof(f610,plain,
! [X0] : v3_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f158]) ).
fof(f611,plain,
! [X0] : v2_orders_2(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f158]) ).
fof(f613,plain,
! [X0] : ~ v3_struct_0(k3_yellow_1(X0)),
inference(cnf_transformation,[],[f158]) ).
fof(f617,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f78]) ).
fof(f683,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,[],[f368]) ).
fof(f684,plain,
! [X2,X3,X0,X1,X4] :
( r2_hidden(sK24(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(cnf_transformation,[],[f371]) ).
fof(f797,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X2,X0,X1)
| m1_relset_1(X2,X0,X1) ),
inference(cnf_transformation,[],[f391]) ).
fof(f799,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,[],[f392]) ).
fof(f800,plain,
! [X2,X0,X1] :
( ~ 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(cnf_transformation,[],[f392]) ).
fof(f803,plain,
! [X0] : k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))) = k1_zfmisc_1(X0),
inference(cnf_transformation,[],[f124]) ).
fof(f804,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f306]) ).
fof(f805,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f308]) ).
fof(f808,plain,
! [X0] : r1_tarski(k1_xboole_0,X0),
inference(cnf_transformation,[],[f128]) ).
fof(f810,plain,
! [X2,X0,X1] :
( r2_lattice3(X0,X2,X1)
| k1_yellow_0(X0,X2) != X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(cnf_transformation,[],[f398]) ).
fof(f814,plain,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f312]) ).
fof(f817,plain,
! [X0,X1] :
( ~ r1_orders_2(X0,k4_yellow_0(X0),X1)
| k4_yellow_0(X0) = X1
| ~ 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,[],[f317]) ).
fof(f821,plain,
v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)),
inference(definition_unfolding,[],[f407,f539]) ).
fof(f822,plain,
m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)),
inference(definition_unfolding,[],[f406,f539]) ).
fof(f826,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,a_1_0_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,a_1_0_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,[],[f540,f539,f539]) ).
fof(f829,plain,
! [X2,X0,X1] :
( ~ m1_relset_1(X2,a_1_0_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_2(X2,a_1_0_waybel22(X0),u1_struct_0(X1))
| v1_funct_1(k2_waybel22(X0,X1,X2)) ),
inference(definition_unfolding,[],[f555,f539,f539]) ).
fof(f830,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,a_1_0_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,a_1_0_waybel22(X0),u1_struct_0(X1)) ),
inference(definition_unfolding,[],[f554,f539,f539]) ).
fof(f831,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,a_1_0_waybel22(X0),u1_struct_0(X1))
| ~ m1_relset_1(X2,a_1_0_waybel22(X0),u1_struct_0(X1)) ),
inference(definition_unfolding,[],[f553,f539,f539]) ).
fof(f838,plain,
! [X0] : ~ v1_xboole_0(k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))))),
inference(definition_unfolding,[],[f617,f803]) ).
fof(f842,plain,
! [X2,X3,X0,X1,X4,X5] :
( r2_hidden(X0,a_4_0_waybel22(X1,X2,X3,X4))
| ~ m1_subset_1(X5,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_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,a_1_0_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,a_1_0_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(definition_unfolding,[],[f683,f803,f539,f539]) ).
fof(f851,plain,
! [X2,X3,X0,X1,X4] :
( ~ m1_subset_1(X4,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1)))))
| ~ 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,a_1_0_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,a_1_0_waybel22(X1),u1_struct_0(X2))
| r2_hidden(sK24(X0,X1,X3,X4),X4) ),
inference(definition_unfolding,[],[f684,f539,f539,f803]) ).
fof(f856,plain,
! [X0,X1] :
( m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1)))))
| ~ r1_tarski(X0,X1) ),
inference(definition_unfolding,[],[f814,f803]) ).
fof(f859,plain,
! [X2] : ~ r2_hidden(X2,k1_xboole_0),
inference(equality_resolution,[],[f536]) ).
fof(f860,plain,
! [X2,X0,X1,X5] :
( ~ 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))
| ~ m1_subset_1(X5,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0)))))
| ~ 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))
| k1_yellow_0(X1,a_4_0_waybel22(X0,X1,X2,X5)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X0))),X1,k2_waybel22(X0,X1,X2),X5)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,a_1_0_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,a_1_0_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,[],[f826]) ).
fof(f864,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,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_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,a_1_0_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,a_1_0_waybel22(X1),u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(X1))))) ),
inference(equality_resolution,[],[f842]) ).
fof(f867,plain,
! [X2,X0] :
( ~ m1_subset_1(k1_yellow_0(X0,X2),u1_struct_0(X0))
| r2_lattice3(X0,X2,k1_yellow_0(X0,X2))
| v3_struct_0(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ l1_orders_2(X0) ),
inference(equality_resolution,[],[f810]) ).
fof(f869,definition,
sF46 = k3_yellow_1(sK8),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f870,plain,
k3_yellow_1(sK8) = sF46,
inference(reorient_equations,[],[f869]) ).
fof(f871,definition,
sF47 = k9_waybel_0(sF46),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f872,plain,
k9_waybel_0(sF46) = sF47,
inference(reorient_equations,[],[f871]) ).
fof(f873,definition,
sF48 = k2_yellow_1(sF47),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f874,plain,
k2_yellow_1(sF47) = sF48,
inference(reorient_equations,[],[f873]) ).
fof(f875,definition,
sF49 = k2_waybel22(sK8,sK9,sK10),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f876,plain,
k2_waybel22(sK8,sK9,sK10) = sF49,
inference(reorient_equations,[],[f875]) ).
fof(f877,definition,
sF50 = k4_yellow_0(sF48),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f878,plain,
k4_yellow_0(sF48) = sF50,
inference(reorient_equations,[],[f877]) ).
fof(f879,definition,
sF51 = k1_waybel_0(sF48,sK9,sF49,sF50),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f880,plain,
k1_waybel_0(sF48,sK9,sF49,sF50) = sF51,
inference(reorient_equations,[],[f879]) ).
fof(f881,definition,
sF52 = k4_yellow_0(sK9),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f882,plain,
k4_yellow_0(sK9) = sF52,
inference(reorient_equations,[],[f881]) ).
fof(f883,plain,
sF51 != sF52,
inference(definition_folding,[],[f409,f882,f880,f878,f874,f872,f870,f876,f874,f872,f870]) ).
fof(f884,definition,
sF53 = a_1_0_waybel22(sK8),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f885,plain,
a_1_0_waybel22(sK8) = sF53,
inference(reorient_equations,[],[f884]) ).
fof(f886,definition,
sF54 = u1_struct_0(sK9),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f887,plain,
u1_struct_0(sK9) = sF54,
inference(reorient_equations,[],[f886]) ).
fof(f888,plain,
v1_funct_2(sK10,sF53,sF54),
inference(definition_folding,[],[f821,f887,f885]) ).
fof(f889,plain,
m2_relset_1(sK10,sF53,sF54),
inference(definition_folding,[],[f822,f887,f885]) ).
fof(f894,plain,
m1_relset_1(sK10,sF53,sF54),
inference(resolution,[],[f797,f889]) ).
fof(f901,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(superposition,[],[f829,f887]) ).
fof(f902,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f901,f405]) ).
fof(f903,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f902,f404]) ).
fof(f904,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f903,f403]) ).
fof(f905,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f904,f402]) ).
fof(f906,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f905,f401]) ).
fof(f907,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f906,f400]) ).
fof(f908,plain,
! [X0,X1] :
( ~ m1_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v1_funct_1(k2_waybel22(X1,sK9,X0)) ),
inference(forward_subsumption_resolution,[],[f907,f399]) ).
fof(f909,plain,
! [X0] :
( v1_funct_1(k2_waybel22(sK8,sK9,X0))
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF53,sF54)
| ~ m1_relset_1(X0,sF53,sF54) ),
inference(superposition,[],[f908,f885]) ).
fof(f910,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(superposition,[],[f830,f876]) ).
fof(f915,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f910,f405]) ).
fof(f918,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f915,f404]) ).
fof(f921,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f918,f403]) ).
fof(f924,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f921,f402]) ).
fof(f926,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f924,f401]) ).
fof(f928,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f926,f400]) ).
fof(f930,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f928,f399]) ).
fof(f931,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f930,f408]) ).
fof(f932,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f931,f887]) ).
fof(f933,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(sF46))),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f932,f870]) ).
fof(f934,plain,
( v1_funct_2(sF49,u1_struct_0(k2_yellow_1(sF47)),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f933,f872]) ).
fof(f935,plain,
( v1_funct_2(sF49,u1_struct_0(sF48),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f934,f874]) ).
fof(f936,plain,
( ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),sF54)
| v1_funct_2(sF49,u1_struct_0(sF48),sF54)
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f935,f887]) ).
fof(f937,plain,
( ~ v1_funct_2(sK10,sF53,sF54)
| v1_funct_2(sF49,u1_struct_0(sF48),sF54)
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f936,f885]) ).
fof(f938,plain,
( v1_funct_2(sF49,u1_struct_0(sF48),sF54)
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f937,f888]) ).
fof(f939,plain,
( ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),sF54)
| v1_funct_2(sF49,u1_struct_0(sF48),sF54) ),
inference(forward_demodulation,[],[f938,f887]) ).
fof(f940,plain,
( ~ m1_relset_1(sK10,sF53,sF54)
| v1_funct_2(sF49,u1_struct_0(sF48),sF54) ),
inference(forward_demodulation,[],[f939,f885]) ).
fof(f941,plain,
v1_funct_2(sF49,u1_struct_0(sF48),sF54),
inference(forward_subsumption_resolution,[],[f940,f894]) ).
fof(f943,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(superposition,[],[f831,f876]) ).
fof(f948,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f943,f405]) ).
fof(f951,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f948,f404]) ).
fof(f954,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f951,f403]) ).
fof(f957,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f954,f402]) ).
fof(f959,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f957,f401]) ).
fof(f961,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f959,f400]) ).
fof(f963,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f961,f399]) ).
fof(f964,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f963,f408]) ).
fof(f965,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f964,f887]) ).
fof(f966,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(sF46))),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f965,f870]) ).
fof(f967,plain,
( m2_relset_1(sF49,u1_struct_0(k2_yellow_1(sF47)),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f966,f872]) ).
fof(f968,plain,
( m2_relset_1(sF49,u1_struct_0(sF48),sF54)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f967,f874]) ).
fof(f969,plain,
( ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),sF54)
| m2_relset_1(sF49,u1_struct_0(sF48),sF54)
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f968,f887]) ).
fof(f970,plain,
( ~ v1_funct_2(sK10,sF53,sF54)
| m2_relset_1(sF49,u1_struct_0(sF48),sF54)
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f969,f885]) ).
fof(f971,plain,
( m2_relset_1(sF49,u1_struct_0(sF48),sF54)
| ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f970,f888]) ).
fof(f972,plain,
( ~ m1_relset_1(sK10,a_1_0_waybel22(sK8),sF54)
| m2_relset_1(sF49,u1_struct_0(sF48),sF54) ),
inference(forward_demodulation,[],[f971,f887]) ).
fof(f973,plain,
( ~ m1_relset_1(sK10,sF53,sF54)
| m2_relset_1(sF49,u1_struct_0(sF48),sF54) ),
inference(forward_demodulation,[],[f972,f885]) ).
fof(f974,plain,
m2_relset_1(sF49,u1_struct_0(sF48),sF54),
inference(forward_subsumption_resolution,[],[f973,f894]) ).
fof(f978,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(superposition,[],[f860,f876]) ).
fof(f984,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f978,f408]) ).
fof(f988,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f984,f405]) ).
fof(f992,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f988,f404]) ).
fof(f996,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f992,f403]) ).
fof(f999,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f996,f402]) ).
fof(f1002,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f999,f401]) ).
fof(f1005,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f1002,f400]) ).
fof(f1007,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f1005,f399]) ).
fof(f1009,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),sF54)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1007,f887]) ).
fof(f1011,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(sF46))),sF54)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1009,f870]) ).
fof(f1012,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(k2_yellow_1(sF47)),sF54)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1011,f872]) ).
fof(f1013,plain,
! [X0] :
( ~ m2_relset_1(sF49,u1_struct_0(sF48),sF54)
| ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1012,f874]) ).
fof(f1014,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f1013,f974]) ).
fof(f1015,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(k9_waybel_0(sF46))))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1014,f870]) ).
fof(f1016,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k2_yellow_1(sF47)))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1015,f872]) ).
fof(f1017,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),u1_struct_0(sK9))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1016,f874]) ).
fof(f1018,plain,
! [X0] :
( ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))),sF54)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1017,f887]) ).
fof(f1019,plain,
! [X0] :
( ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(k9_waybel_0(sF46))),sF54)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1018,f870]) ).
fof(f1020,plain,
! [X0] :
( ~ v1_funct_2(sF49,u1_struct_0(k2_yellow_1(sF47)),sF54)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1019,f872]) ).
fof(f1021,plain,
! [X0] :
( ~ v1_funct_2(sF49,u1_struct_0(sF48),sF54)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1020,f874]) ).
fof(f1022,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))),sK9,sF49,X0)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f1021,f941]) ).
fof(f1023,plain,
! [X0] :
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(k9_waybel_0(sF46)),sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1022,f870]) ).
fof(f1024,plain,
! [X0] :
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(k2_yellow_1(sF47),sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1023,f872]) ).
fof(f1025,plain,
! [X0] :
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1024,f874]) ).
fof(f1026,plain,
! [X0] :
( ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),sF54)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1025,f887]) ).
fof(f1027,plain,
! [X0] :
( ~ v1_funct_2(sK10,sF53,sF54)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_demodulation,[],[f1026,f885]) ).
fof(f1028,plain,
! [X0] :
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49)
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9)) ),
inference(forward_subsumption_resolution,[],[f1027,f888]) ).
fof(f1029,plain,
! [X0] :
( ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),sF54)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49) ),
inference(forward_demodulation,[],[f1028,f887]) ).
fof(f1030,plain,
! [X0] :
( ~ m2_relset_1(sK10,sF53,sF54)
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49) ),
inference(forward_demodulation,[],[f1029,f885]) ).
fof(f1031,plain,
! [X0] :
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ v1_funct_1(sF49) ),
inference(forward_subsumption_resolution,[],[f1030,f889]) ).
fof(f1033,definition,
( spl55_1
<=> v1_funct_1(sF49) ),
introduced(definition,[new_symbols(definition,[spl55_1])],[avatar_definition]) ).
fof(f1035,plain,
( ~ v1_funct_1(sF49)
| spl55_1 ),
inference(avatar_component_clause,[],[f1033]) ).
fof(f1037,definition,
( spl55_2
<=> ! [X0] :
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0)
| ~ m1_subset_1(X0,u1_struct_0(sF48)) ) ),
introduced(definition,[new_symbols(definition,[spl55_2])],[avatar_definition]) ).
fof(f1038,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,X0)) = k1_waybel_0(sF48,sK9,sF49,X0) )
| ~ spl55_2 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1039,plain,
( ~ spl55_1
| spl55_2 ),
inference(avatar_split_clause,[],[f1031,f1037,f1033]) ).
fof(f1052,plain,
! [X0] :
( v3_struct_0(k3_yellow_1(X0))
| ~ v2_orders_2(k3_yellow_1(X0))
| ~ v3_orders_2(k3_yellow_1(X0))
| k9_waybel_0(k3_yellow_1(X0)) = a_1_1_waybel_0(k3_yellow_1(X0)) ),
inference(resolution,[],[f559,f538]) ).
fof(f1054,plain,
! [X0] :
( ~ v2_orders_2(k3_yellow_1(X0))
| ~ v3_orders_2(k3_yellow_1(X0))
| k9_waybel_0(k3_yellow_1(X0)) = a_1_1_waybel_0(k3_yellow_1(X0)) ),
inference(forward_subsumption_resolution,[],[f1052,f613]) ).
fof(f1055,plain,
! [X0] :
( ~ v3_orders_2(k3_yellow_1(X0))
| k9_waybel_0(k3_yellow_1(X0)) = a_1_1_waybel_0(k3_yellow_1(X0)) ),
inference(forward_subsumption_resolution,[],[f1054,f611]) ).
fof(f1056,plain,
! [X0] : k9_waybel_0(k3_yellow_1(X0)) = a_1_1_waybel_0(k3_yellow_1(X0)),
inference(forward_subsumption_resolution,[],[f1055,f610]) ).
fof(f1072,definition,
( spl55_6
<=> sF47 = a_1_1_waybel_0(sF46) ),
introduced(definition,[new_symbols(definition,[spl55_6])],[avatar_definition]) ).
fof(f1074,plain,
( sF47 = a_1_1_waybel_0(sF46)
| ~ spl55_6 ),
inference(avatar_component_clause,[],[f1072]) ).
fof(f1077,plain,
( m1_subset_1(sF50,u1_struct_0(sF48))
| ~ l1_orders_2(sF48) ),
inference(superposition,[],[f561,f878]) ).
fof(f1081,definition,
( spl55_7
<=> l1_orders_2(sF48) ),
introduced(definition,[new_symbols(definition,[spl55_7])],[avatar_definition]) ).
fof(f1082,plain,
( l1_orders_2(sF48)
| ~ spl55_7 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1083,plain,
( ~ l1_orders_2(sF48)
| spl55_7 ),
inference(avatar_component_clause,[],[f1081]) ).
fof(f1085,definition,
( spl55_8
<=> m1_subset_1(sF50,u1_struct_0(sF48)) ),
introduced(definition,[new_symbols(definition,[spl55_8])],[avatar_definition]) ).
fof(f1087,plain,
( m1_subset_1(sF50,u1_struct_0(sF48))
| ~ spl55_8 ),
inference(avatar_component_clause,[],[f1085]) ).
fof(f1088,plain,
( ~ spl55_7
| spl55_8 ),
inference(avatar_split_clause,[],[f1077,f1085,f1081]) ).
fof(f1107,plain,
k9_waybel_0(sF46) = a_1_1_waybel_0(sF46),
inference(superposition,[],[f1056,f870]) ).
fof(f1114,plain,
sF47 = a_1_1_waybel_0(sF46),
inference(forward_demodulation,[],[f1107,f872]) ).
fof(f1115,plain,
spl55_6,
inference(avatar_split_clause,[],[f1114,f1072]) ).
fof(f1118,plain,
l1_orders_2(sF48),
inference(superposition,[],[f557,f874]) ).
fof(f1119,plain,
( $false
| spl55_7 ),
inference(forward_subsumption_resolution,[],[f1118,f1083]) ).
fof(f1120,plain,
spl55_7,
inference(avatar_contradiction_clause,[],[f1119]) ).
fof(f1244,plain,
( v1_funct_1(sF49)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,sF53,sF54)
| ~ m1_relset_1(sK10,sF53,sF54) ),
inference(superposition,[],[f909,f876]) ).
fof(f1245,plain,
( ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,sF53,sF54)
| ~ m1_relset_1(sK10,sF53,sF54)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f1244,f1035]) ).
fof(f1246,plain,
( ~ v1_funct_2(sK10,sF53,sF54)
| ~ m1_relset_1(sK10,sF53,sF54)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f1245,f408]) ).
fof(f1247,plain,
( ~ m1_relset_1(sK10,sF53,sF54)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f1246,f888]) ).
fof(f1248,plain,
( $false
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f1247,f894]) ).
fof(f1249,plain,
spl55_1,
inference(avatar_contradiction_clause,[],[f1248]) ).
fof(f1270,plain,
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,k4_yellow_0(sF48))) = k1_waybel_0(sF48,sK9,sF49,k4_yellow_0(sF48))
| ~ l1_orders_2(sF48)
| ~ spl55_2 ),
inference(resolution,[],[f1038,f561]) ).
fof(f1273,plain,
( k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,k4_yellow_0(sF48))) = k1_waybel_0(sF48,sK9,sF49,k4_yellow_0(sF48))
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f1270,f1082]) ).
fof(f1274,plain,
( k1_waybel_0(sF48,sK9,sF49,sF50) = k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,sF50))
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_demodulation,[],[f1273,f878]) ).
fof(f1275,plain,
( sF51 = k1_yellow_0(sK9,a_4_0_waybel22(sK8,sK9,sK10,sF50))
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_demodulation,[],[f1274,f880]) ).
fof(f1293,plain,
k4_yellow_0(sK9) = k2_yellow_0(sK9,k1_xboole_0),
inference(resolution,[],[f534,f399]) ).
fof(f1297,plain,
sF52 = k2_yellow_0(sK9,k1_xboole_0),
inference(forward_demodulation,[],[f1293,f882]) ).
fof(f1317,plain,
! [X0] :
( m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(sF46))))
| ~ r1_tarski(X0,sK8) ),
inference(superposition,[],[f856,f870]) ).
fof(f1319,plain,
! [X0] :
( m1_subset_1(X0,k4_yellow_0(k2_yellow_1(sF47)))
| ~ r1_tarski(X0,sK8) ),
inference(forward_demodulation,[],[f1317,f872]) ).
fof(f1320,plain,
! [X0] :
( m1_subset_1(X0,k4_yellow_0(sF48))
| ~ r1_tarski(X0,sK8) ),
inference(forward_demodulation,[],[f1319,f874]) ).
fof(f1321,plain,
! [X0] :
( ~ r1_tarski(X0,sK8)
| m1_subset_1(X0,sF50) ),
inference(forward_demodulation,[],[f1320,f878]) ).
fof(f1323,plain,
! [X2,X3,X0,X1,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,a_1_0_waybel22(X1),u1_struct_0(X2))
| ~ m2_relset_1(X3,a_1_0_waybel22(X1),u1_struct_0(X2))
| r2_hidden(sK24(X0,X1,X3,X4),X4)
| ~ r1_tarski(X4,X1) ),
inference(resolution,[],[f851,f856]) ).
fof(f1415,plain,
! [X0] :
( ~ r1_orders_2(sK9,sF52,X0)
| sF52 = X0
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| v3_struct_0(sK9)
| ~ v4_orders_2(sK9)
| ~ v2_yellow_0(sK9)
| ~ l1_orders_2(sK9) ),
inference(superposition,[],[f817,f882]) ).
fof(f1417,plain,
! [X0] :
( ~ r1_orders_2(sK9,sF52,X0)
| sF52 = X0
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ v4_orders_2(sK9)
| ~ v2_yellow_0(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f1415,f405]) ).
fof(f1418,plain,
! [X0] :
( ~ r1_orders_2(sK9,sF52,X0)
| sF52 = X0
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ v2_yellow_0(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f1417,f402]) ).
fof(f1419,plain,
! [X0] :
( ~ r1_orders_2(sK9,sF52,X0)
| sF52 = X0
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ v2_yellow_0(sK9) ),
inference(forward_subsumption_resolution,[],[f1418,f399]) ).
fof(f1420,plain,
! [X0] :
( ~ m1_subset_1(X0,sF54)
| ~ r1_orders_2(sK9,sF52,X0)
| sF52 = X0
| ~ v2_yellow_0(sK9) ),
inference(forward_demodulation,[],[f1419,f887]) ).
fof(f1422,definition,
( spl55_14
<=> v2_yellow_0(sK9) ),
introduced(definition,[new_symbols(definition,[spl55_14])],[avatar_definition]) ).
fof(f1424,plain,
( ~ v2_yellow_0(sK9)
| spl55_14 ),
inference(avatar_component_clause,[],[f1422]) ).
fof(f1426,definition,
( spl55_15
<=> ! [X0] :
( ~ m1_subset_1(X0,sF54)
| sF52 = X0
| ~ r1_orders_2(sK9,sF52,X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_15])],[avatar_definition]) ).
fof(f1427,plain,
( ! [X0] :
( ~ r1_orders_2(sK9,sF52,X0)
| sF52 = X0
| ~ m1_subset_1(X0,sF54) )
| ~ spl55_15 ),
inference(avatar_component_clause,[],[f1426]) ).
fof(f1428,plain,
( ~ spl55_14
| spl55_15 ),
inference(avatar_split_clause,[],[f1420,f1426,f1422]) ).
fof(f1666,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK9,X0),sF54)
| r2_lattice3(sK9,X0,k1_yellow_0(sK9,X0))
| v3_struct_0(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9) ),
inference(superposition,[],[f867,f887]) ).
fof(f1667,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK9,X0),sF54)
| r2_lattice3(sK9,X0,k1_yellow_0(sK9,X0))
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f1666,f405]) ).
fof(f1669,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK9,X0),sF54)
| r2_lattice3(sK9,X0,k1_yellow_0(sK9,X0))
| ~ v3_lattice3(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f1667,f402]) ).
fof(f1671,plain,
! [X0] :
( ~ m1_subset_1(k1_yellow_0(sK9,X0),sF54)
| r2_lattice3(sK9,X0,k1_yellow_0(sK9,X0))
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f1669,f401]) ).
fof(f1673,plain,
! [X0] :
( r2_lattice3(sK9,X0,k1_yellow_0(sK9,X0))
| ~ m1_subset_1(k1_yellow_0(sK9,X0),sF54) ),
inference(forward_subsumption_resolution,[],[f1671,f399]) ).
fof(f1681,definition,
( spl55_26
<=> m1_subset_1(sF51,sF54) ),
introduced(definition,[new_symbols(definition,[spl55_26])],[avatar_definition]) ).
fof(f1682,plain,
( m1_subset_1(sF51,sF54)
| ~ spl55_26 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f1683,plain,
( ~ m1_subset_1(sF51,sF54)
| spl55_26 ),
inference(avatar_component_clause,[],[f1681]) ).
fof(f2024,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| r1_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ m1_subset_1(k1_yellow_0(sK9,X1),u1_struct_0(sK9))
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(resolution,[],[f543,f1673]) ).
fof(f2028,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| r1_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_subsumption_resolution,[],[f2024,f552]) ).
fof(f2029,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| r1_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_subsumption_resolution,[],[f2028,f399]) ).
fof(f2030,plain,
! [X0,X1] :
( r1_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_demodulation,[],[f2029,f887]) ).
fof(f2257,plain,
( v3_struct_0(sK9)
| ~ v3_lattice3(sK9)
| v1_lattice3(sK9) ),
inference(resolution,[],[f455,f399]) ).
fof(f2261,plain,
( ~ v3_lattice3(sK9)
| v1_lattice3(sK9) ),
inference(forward_subsumption_resolution,[],[f2257,f405]) ).
fof(f2263,plain,
v1_lattice3(sK9),
inference(forward_subsumption_resolution,[],[f2261,f401]) ).
fof(f2358,plain,
~ v1_xboole_0(k4_yellow_0(k2_yellow_1(k9_waybel_0(sF46)))),
inference(superposition,[],[f838,f870]) ).
fof(f2360,plain,
~ v1_xboole_0(k4_yellow_0(k2_yellow_1(sF47))),
inference(forward_demodulation,[],[f2358,f872]) ).
fof(f2361,plain,
~ v1_xboole_0(k4_yellow_0(sF48)),
inference(forward_demodulation,[],[f2360,f874]) ).
fof(f2362,plain,
~ v1_xboole_0(sF50),
inference(forward_demodulation,[],[f2361,f878]) ).
fof(f2392,plain,
( m1_subset_1(sF51,u1_struct_0(sK9))
| ~ l1_orders_2(sK9)
| ~ spl55_2
| ~ spl55_7 ),
inference(superposition,[],[f552,f1275]) ).
fof(f2393,plain,
! [X0] :
( m1_subset_1(k1_yellow_0(sK9,X0),sF54)
| ~ l1_orders_2(sK9) ),
inference(superposition,[],[f552,f887]) ).
fof(f2396,plain,
! [X0] : m1_subset_1(k1_yellow_0(sK9,X0),sF54),
inference(forward_subsumption_resolution,[],[f2393,f399]) ).
fof(f2397,plain,
( m1_subset_1(sF51,u1_struct_0(sK9))
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f2392,f399]) ).
fof(f2404,plain,
( m1_subset_1(sF51,sF54)
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_demodulation,[],[f2397,f887]) ).
fof(f2407,plain,
( $false
| ~ spl55_2
| ~ spl55_7
| spl55_26 ),
inference(forward_subsumption_resolution,[],[f2404,f1683]) ).
fof(f2408,plain,
( ~ spl55_2
| ~ spl55_7
| spl55_26 ),
inference(avatar_contradiction_clause,[],[f2407]) ).
fof(f2517,plain,
m1_subset_1(k1_xboole_0,sF50),
inference(resolution,[],[f808,f1321]) ).
fof(f2563,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ m1_subset_1(k1_yellow_0(sK9,X1),u1_struct_0(sK9))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(resolution,[],[f800,f2030]) ).
fof(f2567,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_subsumption_resolution,[],[f2563,f552]) ).
fof(f2570,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_subsumption_resolution,[],[f2567,f405]) ).
fof(f2573,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_subsumption_resolution,[],[f2570,f404]) ).
fof(f2576,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54)
| ~ m1_subset_1(k1_yellow_0(sK9,X1),sF54) ),
inference(forward_subsumption_resolution,[],[f2573,f399]) ).
fof(f2579,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ m1_subset_1(X0,u1_struct_0(sK9))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54) ),
inference(forward_subsumption_resolution,[],[f2576,f2396]) ).
fof(f2581,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF54)
| r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,sF54) ),
inference(forward_demodulation,[],[f2579,f887]) ).
fof(f2582,plain,
! [X0,X1] :
( r3_orders_2(sK9,X0,k1_yellow_0(sK9,X1))
| ~ m1_subset_1(X0,sF54)
| ~ r2_hidden(X0,X1) ),
inference(duplicate_literal_removal,[],[f2581]) ).
fof(f2677,plain,
! [X0] :
( m1_subset_1(k2_yellow_0(sK9,X0),sF54)
| ~ l1_orders_2(sK9) ),
inference(superposition,[],[f556,f887]) ).
fof(f2678,plain,
! [X0] : m1_subset_1(k2_yellow_0(sK9,X0),sF54),
inference(forward_subsumption_resolution,[],[f2677,f399]) ).
fof(f2745,plain,
( ! [X0] :
( ~ r2_hidden(X0,a_4_0_waybel22(sK8,sK9,sK10,sF50))
| ~ m1_subset_1(X0,sF54)
| r3_orders_2(sK9,X0,sF51) )
| ~ spl55_2
| ~ spl55_7 ),
inference(superposition,[],[f2582,f1275]) ).
fof(f2967,plain,
( v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_lattice3(sK9)
| v24_waybel_0(sK9) ),
inference(resolution,[],[f413,f399]) ).
fof(f2971,plain,
( ~ v2_orders_2(sK9)
| ~ v3_lattice3(sK9)
| v24_waybel_0(sK9) ),
inference(forward_subsumption_resolution,[],[f2967,f405]) ).
fof(f2973,plain,
( ~ v3_lattice3(sK9)
| v24_waybel_0(sK9) ),
inference(forward_subsumption_resolution,[],[f2971,f404]) ).
fof(f2975,plain,
v24_waybel_0(sK9),
inference(forward_subsumption_resolution,[],[f2973,f401]) ).
fof(f3116,plain,
( r2_hidden(k1_xboole_0,sF50)
| v1_xboole_0(sF50) ),
inference(resolution,[],[f805,f2517]) ).
fof(f3163,plain,
r2_hidden(k1_xboole_0,sF50),
inference(forward_subsumption_resolution,[],[f3116,f2362]) ).
fof(f3314,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(resolution,[],[f2745,f864]) ).
fof(f3321,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3314,f405]) ).
fof(f3322,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3321,f404]) ).
fof(f3323,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3322,f403]) ).
fof(f3324,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3323,f402]) ).
fof(f3325,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3324,f401]) ).
fof(f3326,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3325,f400]) ).
fof(f3327,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3326,f399]) ).
fof(f3328,plain,
( ! [X0] :
( ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3327,f408]) ).
fof(f3329,plain,
( ! [X0] :
( r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8)))))
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3328,f2678]) ).
fof(f3330,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(a_1_1_waybel_0(k3_yellow_1(sK8)))))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3329,f1056]) ).
fof(f3331,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(a_1_1_waybel_0(sF46))))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3330,f870]) ).
fof(f3332,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_yellow_0(k2_yellow_1(sF47)))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3331,f1074]) ).
fof(f3333,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k4_yellow_0(sF48))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3332,f874]) ).
fof(f3334,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF50)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3333,f878]) ).
fof(f3335,plain,
( ! [X0] :
( r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3334,f804]) ).
fof(f3336,plain,
( ! [X0] :
( ~ v1_funct_2(sK10,a_1_0_waybel22(sK8),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3335,f887]) ).
fof(f3337,plain,
( ! [X0] :
( ~ v1_funct_2(sK10,sF53,sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3336,f885]) ).
fof(f3338,plain,
( ! [X0] :
( r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),u1_struct_0(sK9))
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3337,f888]) ).
fof(f3339,plain,
( ! [X0] :
( ~ m2_relset_1(sK10,a_1_0_waybel22(sK8),sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3338,f887]) ).
fof(f3340,plain,
( ! [X0] :
( ~ m2_relset_1(sK10,sF53,sF54)
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3339,f885]) ).
fof(f3341,plain,
( ! [X0] :
( r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50)
| ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(k9_waybel_0(k3_yellow_1(sK8))))) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_subsumption_resolution,[],[f3340,f889]) ).
fof(f3342,plain,
( ! [X0] :
( ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(a_1_1_waybel_0(k3_yellow_1(sK8)))))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3341,f1056]) ).
fof(f3343,plain,
( ! [X0] :
( ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(a_1_1_waybel_0(sF46))))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3342,f870]) ).
fof(f3344,plain,
( ! [X0] :
( ~ m1_subset_1(sF50,u1_struct_0(k2_yellow_1(sF47)))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3343,f1074]) ).
fof(f3345,plain,
( ! [X0] :
( ~ m1_subset_1(sF50,u1_struct_0(sF48))
| r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7 ),
inference(forward_demodulation,[],[f3344,f874]) ).
fof(f3346,plain,
( ! [X0] :
( r3_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f3345,f1087]) ).
fof(f3758,plain,
( ~ v2_orders_2(sK9)
| v2_yellow_0(sK9)
| ~ v24_waybel_0(sK9)
| ~ l1_orders_2(sK9) ),
inference(resolution,[],[f530,f2263]) ).
fof(f3762,plain,
( v2_yellow_0(sK9)
| ~ v24_waybel_0(sK9)
| ~ l1_orders_2(sK9) ),
inference(forward_subsumption_resolution,[],[f3758,f404]) ).
fof(f3764,plain,
( ~ v24_waybel_0(sK9)
| ~ l1_orders_2(sK9)
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f3762,f1424]) ).
fof(f3766,plain,
( ~ l1_orders_2(sK9)
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f3764,f2975]) ).
fof(f3769,plain,
( $false
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f3766,f399]) ).
fof(f3770,plain,
spl55_14,
inference(avatar_contradiction_clause,[],[f3769]) ).
fof(f10527,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF50)
| r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),u1_struct_0(sK9))
| ~ m1_subset_1(sF51,u1_struct_0(sK9)) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(resolution,[],[f3346,f799]) ).
fof(f10528,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF50)
| r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| v3_struct_0(sK9)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(sF51,u1_struct_0(sK9)) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f10527,f556]) ).
fof(f10529,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF50)
| r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ v2_orders_2(sK9)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(sF51,u1_struct_0(sK9)) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f10528,f405]) ).
fof(f10530,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF50)
| r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ l1_orders_2(sK9)
| ~ m1_subset_1(sF51,u1_struct_0(sK9)) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f10529,f404]) ).
fof(f10531,plain,
( ! [X0] :
( ~ r2_hidden(X0,sF50)
| r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ m1_subset_1(sF51,u1_struct_0(sK9)) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f10530,f399]) ).
fof(f10532,plain,
( ! [X0] :
( ~ m1_subset_1(sF51,sF54)
| ~ r2_hidden(X0,sF50)
| r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8 ),
inference(forward_demodulation,[],[f10531,f887]) ).
fof(f10533,plain,
( ! [X0] :
( r1_orders_2(sK9,k2_yellow_0(sK9,a_4_1_waybel22(sK8,sK9,sK10,X0)),sF51)
| ~ r2_hidden(X0,sF50) )
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f10532,f1682]) ).
fof(f13088,plain,
! [X2,X3,X0,X1] :
( r2_hidden(sK24(sK11(a_4_1_waybel22(X0,X1,X2,X3)),X0,X2,X3),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,a_1_0_waybel22(X0),u1_struct_0(X1))
| ~ m2_relset_1(X2,a_1_0_waybel22(X0),u1_struct_0(X1))
| k1_xboole_0 = a_4_1_waybel22(X0,X1,X2,X3)
| ~ r1_tarski(X3,X0) ),
inference(resolution,[],[f537,f1323]) ).
fof(f13246,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,a_1_0_waybel22(X2),u1_struct_0(X0))
| ~ m2_relset_1(X1,a_1_0_waybel22(X2),u1_struct_0(X0))
| k1_xboole_0 = a_4_1_waybel22(X2,X0,X1,k1_xboole_0)
| ~ r1_tarski(k1_xboole_0,X2) ),
inference(resolution,[],[f13088,f859]) ).
fof(f13341,plain,
! [X2,X0,X1] :
( ~ m2_relset_1(X1,a_1_0_waybel22(X2),u1_struct_0(X0))
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ v3_waybel_3(X0)
| ~ l1_orders_2(X0)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,a_1_0_waybel22(X2),u1_struct_0(X0))
| v3_struct_0(X0)
| k1_xboole_0 = a_4_1_waybel22(X2,X0,X1,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13246,f808]) ).
fof(f13371,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v2_orders_2(sK9)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(superposition,[],[f13341,f887]) ).
fof(f13372,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v3_orders_2(sK9)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13371,f404]) ).
fof(f13374,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v4_orders_2(sK9)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13372,f403]) ).
fof(f13376,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v3_lattice3(sK9)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13374,f402]) ).
fof(f13377,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v3_waybel_3(sK9)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13376,f401]) ).
fof(f13378,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ l1_orders_2(sK9)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13377,f400]) ).
fof(f13379,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| v3_struct_0(sK9)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13378,f399]) ).
fof(f13380,plain,
! [X0,X1] :
( ~ m2_relset_1(X0,a_1_0_waybel22(X1),sF54)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,a_1_0_waybel22(X1),sF54)
| k1_xboole_0 = a_4_1_waybel22(X1,sK9,X0,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f13379,f405]) ).
fof(f13381,plain,
! [X0] :
( ~ m2_relset_1(X0,sF53,sF54)
| ~ v1_funct_1(X0)
| ~ v1_funct_2(X0,sF53,sF54)
| k1_xboole_0 = a_4_1_waybel22(sK8,sK9,X0,k1_xboole_0) ),
inference(superposition,[],[f13380,f885]) ).
fof(f14217,plain,
( ~ v1_funct_1(sK10)
| ~ v1_funct_2(sK10,sF53,sF54)
| k1_xboole_0 = a_4_1_waybel22(sK8,sK9,sK10,k1_xboole_0) ),
inference(resolution,[],[f13381,f889]) ).
fof(f14218,plain,
( ~ v1_funct_2(sK10,sF53,sF54)
| k1_xboole_0 = a_4_1_waybel22(sK8,sK9,sK10,k1_xboole_0) ),
inference(forward_subsumption_resolution,[],[f14217,f408]) ).
fof(f14219,plain,
k1_xboole_0 = a_4_1_waybel22(sK8,sK9,sK10,k1_xboole_0),
inference(forward_subsumption_resolution,[],[f14218,f888]) ).
fof(f14220,plain,
( r1_orders_2(sK9,k2_yellow_0(sK9,k1_xboole_0),sF51)
| ~ r2_hidden(k1_xboole_0,sF50)
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_26 ),
inference(superposition,[],[f10533,f14219]) ).
fof(f14249,plain,
( r1_orders_2(sK9,k2_yellow_0(sK9,k1_xboole_0),sF51)
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f14220,f3163]) ).
fof(f14253,plain,
( r1_orders_2(sK9,sF52,sF51)
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_26 ),
inference(forward_demodulation,[],[f14249,f1297]) ).
fof(f14298,plain,
( sF51 = sF52
| ~ m1_subset_1(sF51,sF54)
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_15
| ~ spl55_26 ),
inference(resolution,[],[f14253,f1427]) ).
fof(f14300,plain,
( ~ m1_subset_1(sF51,sF54)
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_15
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f14298,f883]) ).
fof(f14301,plain,
( $false
| ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_15
| ~ spl55_26 ),
inference(forward_subsumption_resolution,[],[f14300,f1682]) ).
fof(f14302,plain,
( ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_15
| ~ spl55_26 ),
inference(avatar_contradiction_clause,[],[f14301]) ).
cnf(s1,plain,
( ~ spl55_1
| spl55_2 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s3,plain,
( ~ spl55_7
| spl55_8 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s4,plain,
spl55_6,
inference(sat_conversion,[],[f1115]) ).
cnf(s5,plain,
spl55_7,
inference(sat_conversion,[],[f1120]) ).
cnf(s8,plain,
spl55_1,
inference(sat_conversion,[],[f1249]) ).
cnf(s9,plain,
( ~ spl55_14
| spl55_15 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s20,plain,
( ~ spl55_2
| ~ spl55_7
| spl55_26 ),
inference(sat_conversion,[],[f2408]) ).
cnf(s34,plain,
spl55_14,
inference(sat_conversion,[],[f3770]) ).
cnf(s242,plain,
( ~ spl55_2
| ~ spl55_6
| ~ spl55_7
| ~ spl55_8
| ~ spl55_15
| ~ spl55_26 ),
inference(sat_conversion,[],[f14302]) ).
cnf(s275,plain,
spl55_15,
inference(rat,[],[s9,s34]) ).
cnf(s290,plain,
spl55_8,
inference(rat,[],[s3,s5]) ).
cnf(s293,plain,
spl55_2,
inference(rat,[],[s1,s8]) ).
cnf(s294,plain,
~ spl55_26,
inference(rat,[],[s242,s290,s275,s4,s5,s293]) ).
cnf(s296,plain,
$false,
inference(rat,[],[s20,s5,s294,s293]) ).
fof(f14303,plain,
$false,
inference(avatar_sat_refutation,[],[s296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT350+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.34 % Computer : n012.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.02/0.34 % CPULimit : 300
% 0.02/0.34 % WCLimit : 300
% 0.02/0.34 % DateTime : Sun Sep 27 14:54:20 UTC 2026
% 0.02/0.34 % CPUTime :
% 0.02/0.34 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.02/0.37 Running first-order theorem proving
% 0.02/0.37 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.51/2.68 % (2458692)Detected formulas, will run a generic FOF schedule.
% 12.51/2.68 % (2458703)dis-21_1_sil=8000:lcm=predicate:random_seed=2184815219:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.51/2.68 % (2458699)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=469753007:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.51/2.68 % (2458698)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=752292754:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.51/2.68 % (2458703)Instruction limit reached!
% 12.51/2.68 % (2458703)------------------------------
% 12.51/2.68 % (2458703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.68 % (2458703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.68 % (2458703)CaDiCaL version: 2.1.3
% 12.51/2.68 % (2458703)Termination reason: Instruction limit
% 12.51/2.68 % (2458703)Termination phase: Saturation
% 12.51/2.68 % (2458703)Time elapsed: 0.044 s
% 12.51/2.68 % (2458703)Peak memory usage: 91 MB
% 12.51/2.68 % (2458703)Instructions burned: 129 (million)
% 12.51/2.68 % (2458697)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=841777954:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.51/2.68 % (2458701)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1626848557:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.51/2.68 % (2458700)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1910471614:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.51/2.68 % (2458700)Refutation not found, incomplete strategy
% 12.51/2.68 % (2458700)------------------------------
% 12.51/2.68 % (2458700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.68 % (2458700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.68 % (2458700)CaDiCaL version: 2.1.3
% 12.51/2.68 % (2458700)Termination reason: Refutation not found, incomplete strategy
% 12.51/2.68 % (2458700)Time elapsed: 0.002 s
% 12.51/2.68 % (2458700)Peak memory usage: 88 MB
% 12.51/2.68 % (2458700)Instructions burned: 2 (million)
% 12.51/2.68 % (2458702)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3547020313:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.51/2.68 % (2458701)Instruction limit reached!
% 12.51/2.68 % (2458701)------------------------------
% 12.51/2.68 % (2458701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.68 % (2458701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.68 % (2458701)CaDiCaL version: 2.1.3
% 12.51/2.68 % (2458701)Termination reason: Instruction limit
% 12.51/2.68 % (2458701)Termination phase: Saturation
% 12.51/2.68 % (2458701)Time elapsed: 0.060 s
% 12.51/2.68 % (2458701)Peak memory usage: 88 MB
% 12.51/2.68 % (2458701)Instructions burned: 119 (million)
% 12.51/2.68 % (2458702)Instruction limit reached!
% 12.51/2.68 % (2458702)------------------------------
% 12.51/2.68 % (2458702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.68 % (2458702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.68 % (2458702)CaDiCaL version: 2.1.3
% 12.51/2.68 % (2458702)Termination reason: Instruction limit
% 12.51/2.68 % (2458702)Termination phase: Saturation
% 12.51/2.68 % (2458702)Time elapsed: 0.079 s
% 12.51/2.68 % (2458702)Peak memory usage: 90 MB
% 12.51/2.68 % (2458702)Instructions burned: 139 (million)
% 12.51/2.68 % (2458707)lrs+10_1_sil=8000:sp=occurrence:random_seed=1554485855:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 12.51/2.68 % (2458700)------------------------------
% 12.51/2.68 % (2458700)------------------------------
% 12.51/2.68 % (2458712)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4008669692:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.51/2.68 % (2458712)Refutation not found, incomplete strategy
% 12.51/2.68 % (2458712)------------------------------
% 12.51/2.68 % (2458712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.68 % (2458712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.95/3.65 % (2458712)CaDiCaL version: 2.1.3
% 19.95/3.65 % (2458712)Termination reason: Refutation not found, incomplete strategy
% 19.95/3.65 % (2458712)Time elapsed: 0.007 s
% 19.95/3.65 % (2458712)Peak memory usage: 89 MB
% 19.95/3.65 % (2458712)Instructions burned: 11 (million)
% 19.95/3.65 % (2458707)Instruction limit reached!
% 19.95/3.65 % (2458707)------------------------------
% 19.95/3.65 % (2458707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.95/3.65 % (2458707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.95/3.65 % (2458707)CaDiCaL version: 2.1.3
% 19.95/3.65 % (2458707)Termination reason: Instruction limit
% 19.95/3.65 % (2458707)Termination phase: Saturation
% 19.95/3.65 % (2458707)Time elapsed: 0.149 s
% 19.95/3.65 % (2458707)Peak memory usage: 91 MB
% 19.95/3.65 % (2458707)Instructions burned: 287 (million)
% 19.95/3.65 % (2458713)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3012125740:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 19.95/3.65 % (2458715)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=495086564:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.95/3.65 % (2458713)Instruction limit reached!
% 19.95/3.65 % (2458713)------------------------------
% 19.95/3.65 % (2458713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.95/3.65 % (2458713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.95/3.65 % (2458713)CaDiCaL version: 2.1.3
% 19.95/3.65 % (2458713)Termination reason: Instruction limit
% 19.95/3.65 % (2458713)Termination phase: Saturation
% 19.95/3.65 % (2458713)Time elapsed: 0.151 s
% 19.95/3.65 % (2458713)Peak memory usage: 91 MB
% 19.95/3.65 % (2458713)Instructions burned: 327 (million)
% 19.95/3.65 % (2458717)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=556397270:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 19.95/3.65 % (2458712)------------------------------
% 19.95/3.65 % (2458712)------------------------------
% 19.95/3.65 % (2458717)Refutation not found, incomplete strategy
% 19.95/3.65 % (2458717)------------------------------
% 19.95/3.65 % (2458717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.95/3.65 % (2458717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.95/3.65 % (2458717)CaDiCaL version: 2.1.3
% 19.95/3.65 % (2458717)Termination reason: Refutation not found, incomplete strategy
% 19.95/3.65 % (2458717)Time elapsed: 0.010 s
% 19.95/3.65 % (2458717)Peak memory usage: 89 MB
% 19.95/3.65 % (2458717)Instructions burned: 18 (million)
% 19.95/3.65 % (2458715)Instruction limit reached!
% 19.95/3.65 % (2458715)------------------------------
% 19.95/3.65 % (2458715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.95/3.65 % (2458715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.95/3.65 % (2458715)CaDiCaL version: 2.1.3
% 19.95/3.65 % (2458715)Termination reason: Instruction limit
% 19.95/3.65 % (2458715)Termination phase: Saturation
% 19.95/3.65 % (2458715)Time elapsed: 0.127 s
% 19.95/3.65 % (2458715)Peak memory usage: 91 MB
% 19.95/3.65 % (2458715)Instructions burned: 248 (million)
% 19.95/3.65 % (2458720)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=242970905:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.95/3.65 % (2458722)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1704094202:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 19.95/3.65 % (2458723)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1285742848:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.95/3.65 % (2458717)------------------------------
% 19.95/3.65 % (2458717)------------------------------
% 19.95/3.65 % (2458723)Instruction limit reached!
% 19.95/3.65 % (2458723)------------------------------
% 19.95/3.65 % (2458723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.95/3.65 % (2458723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.95/3.65 % (2458723)CaDiCaL version: 2.1.3
% 19.95/3.65 % (2458723)Termination reason: Instruction limit
% 19.95/3.65 % (2458723)Termination phase: Saturation
% 19.95/3.65 % (2458723)Time elapsed: 0.038 s
% 19.95/3.65 % (2458723)Peak memory usage: 89 MB
% 19.95/3.65 % (2458723)Instructions burned: 128 (million)
% 19.95/3.65 % (2458722)Instruction limit reached!
% 19.95/3.65 % (2458722)------------------------------
% 19.95/3.65 % (2458722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458722)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458722)Termination reason: Instruction limit
% 25.96/4.45 % (2458722)Termination phase: Saturation
% 25.96/4.45 % (2458722)Time elapsed: 0.063 s
% 25.96/4.45 % (2458722)Peak memory usage: 91 MB
% 25.96/4.45 % (2458722)Instructions burned: 114 (million)
% 25.96/4.45 % (2458727)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=360973563:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 25.96/4.45 % (2458727)Refutation not found, incomplete strategy
% 25.96/4.45 % (2458727)------------------------------
% 25.96/4.45 % (2458727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458727)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458727)Termination reason: Refutation not found, incomplete strategy
% 25.96/4.45 % (2458727)Time elapsed: 0.004 s
% 25.96/4.45 % (2458727)Peak memory usage: 89 MB
% 25.96/4.45 % (2458727)Instructions burned: 6 (million)
% 25.96/4.45 % (2458729)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2832087716:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 25.96/4.45 % (2458728)lrs+10_1_sil=8000:sp=occurrence:random_seed=968499188:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 25.96/4.45 % (2458729)Refutation not found, incomplete strategy
% 25.96/4.45 % (2458729)------------------------------
% 25.96/4.45 % (2458729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458729)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458729)Termination reason: Refutation not found, incomplete strategy
% 25.96/4.45 % (2458729)Time elapsed: 0.011 s
% 25.96/4.45 % (2458729)Peak memory usage: 89 MB
% 25.96/4.45 % (2458729)Instructions burned: 20 (million)
% 25.96/4.45 % (2458727)------------------------------
% 25.96/4.45 % (2458727)------------------------------
% 25.96/4.45 % (2458729)------------------------------
% 25.96/4.45 % (2458729)------------------------------
% 25.96/4.45 % (2458735)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2082057249:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 25.96/4.45 % (2458728)Instruction limit reached!
% 25.96/4.45 % (2458728)------------------------------
% 25.96/4.45 % (2458728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458728)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458728)Termination reason: Instruction limit
% 25.96/4.45 % (2458728)Termination phase: Saturation
% 25.96/4.45 % (2458728)Time elapsed: 0.418 s
% 25.96/4.45 % (2458728)Peak memory usage: 98 MB
% 25.96/4.45 % (2458728)Instructions burned: 908 (million)
% 25.96/4.45 % (2458736)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=197623891:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 25.96/4.45 % (2458736)Instruction limit reached!
% 25.96/4.45 % (2458736)------------------------------
% 25.96/4.45 % (2458736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458736)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458736)Termination reason: Instruction limit
% 25.96/4.45 % (2458736)Termination phase: Saturation
% 25.96/4.45 % (2458736)Time elapsed: 0.068 s
% 25.96/4.45 % (2458736)Peak memory usage: 91 MB
% 25.96/4.45 % (2458736)Instructions burned: 135 (million)
% 25.96/4.45 % (2458738)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3133118539:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 25.96/4.45 % (2458720)Instruction limit reached!
% 25.96/4.45 % (2458720)------------------------------
% 25.96/4.45 % (2458720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458720)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458720)Termination reason: Instruction limit
% 25.96/4.45 % (2458720)Termination phase: Saturation
% 25.96/4.45 % (2458720)Time elapsed: 1.039 s
% 25.96/4.45 % (2458720)Peak memory usage: 140 MB
% 25.96/4.45 % (2458720)Instructions burned: 2351 (million)
% 25.96/4.45 % (2458740)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1145519810:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 25.96/4.45 % (2458743)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=4016725470:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 25.96/4.45 % (2458738)Instruction limit reached!
% 25.96/4.45 % (2458738)------------------------------
% 25.96/4.45 % (2458738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458738)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458738)Termination reason: Instruction limit
% 25.96/4.45 % (2458738)Termination phase: Saturation
% 25.96/4.45 % (2458738)Time elapsed: 0.260 s
% 25.96/4.45 % (2458738)Peak memory usage: 93 MB
% 25.96/4.45 % (2458738)Instructions burned: 594 (million)
% 25.96/4.45 % (2458743)Instruction limit reached!
% 25.96/4.45 % (2458743)------------------------------
% 25.96/4.45 % (2458743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458743)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458743)Termination reason: Instruction limit
% 25.96/4.45 % (2458743)Termination phase: Saturation
% 25.96/4.45 % (2458743)Time elapsed: 0.056 s
% 25.96/4.45 % (2458743)Peak memory usage: 90 MB
% 25.96/4.45 % (2458743)Instructions burned: 127 (million)
% 25.96/4.45 % (2458745)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=617748170:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 25.96/4.45 % (2458745)Instruction limit reached!
% 25.96/4.45 % (2458745)------------------------------
% 25.96/4.45 % (2458745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458745)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458745)Termination reason: Instruction limit
% 25.96/4.45 % (2458745)Termination phase: Saturation
% 25.96/4.45 % (2458745)Time elapsed: 0.068 s
% 25.96/4.45 % (2458745)Peak memory usage: 91 MB
% 25.96/4.45 % (2458745)Instructions burned: 135 (million)
% 25.96/4.45 % (2458746)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2780222778:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 25.96/4.45 % (2458746)Refutation not found, incomplete strategy
% 25.96/4.45 % (2458746)------------------------------
% 25.96/4.45 % (2458746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458746)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458746)Termination reason: Refutation not found, incomplete strategy
% 25.96/4.45 % (2458746)Time elapsed: 0.004 s
% 25.96/4.45 % (2458746)Peak memory usage: 88 MB
% 25.96/4.45 % (2458746)Instructions burned: 5 (million)
% 25.96/4.45 % (2458748)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4005520310:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 25.96/4.45 % (2458746)------------------------------
% 25.96/4.45 % (2458746)------------------------------
% 25.96/4.45 % (2458748)Instruction limit reached!
% 25.96/4.45 % (2458748)------------------------------
% 25.96/4.45 % (2458748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458748)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458748)Termination reason: Instruction limit
% 25.96/4.45 % (2458748)Termination phase: Saturation
% 25.96/4.45 % (2458748)Time elapsed: 0.210 s
% 25.96/4.45 % (2458748)Peak memory usage: 93 MB
% 25.96/4.45 % (2458748)Instructions burned: 432 (million)
% 25.96/4.45 % (2458751)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=2389188260:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 25.96/4.45 % (2458752)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=299300801:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 25.96/4.45 % (2458752)Instruction limit reached!
% 25.96/4.45 % (2458752)------------------------------
% 25.96/4.45 % (2458752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.96/4.45 % (2458752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.96/4.45 % (2458752)CaDiCaL version: 2.1.3
% 25.96/4.45 % (2458752)Termination reason: Instruction limit
% 25.96/4.45 % (2458752)Termination phase: Saturation
% 25.96/4.45 % (2458752)Time elapsed: 0.086 s
% 25.96/4.45 % (2458752)Peak memory usage: 91 MB
% 25.96/4.45 % (2458752)Instructions burned: 150 (million)
% 25.96/4.45 % (2458755)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1973161594:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 25.96/4.45 % (2458697)First to succeed.
% 25.96/4.45 % (2458697)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2458692"
% 25.96/4.45 % (2458740)Also succeeded, but the first one will report.
% 25.96/4.45 % (2458697)Refutation found. Thanks to Tanya!
% 25.96/4.45 % SZS status Theorem for theBenchmark
% 25.96/4.45 % SZS output start Proof for theBenchmark
% See solution above
% 26.41/4.59 % (2458697)------------------------------
% 26.41/4.59 % (2458697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.41/4.59 % (2458697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.41/4.59 % (2458697)CaDiCaL version: 2.1.3
% 26.41/4.59 % (2458697)Termination reason: Refutation
% 26.41/4.59 % (2458697)Time elapsed: 3.231 s
% 26.41/4.59 % (2458697)Peak memory usage: 164 MB
% 26.41/4.59 % (2458697)Instructions burned: 6016 (million)
% 26.41/4.59 % (2458697)------------------------------
% 26.41/4.59 % (2458697)------------------------------
% 26.41/4.59 % (2458692)Success in time 3.698 s
% 26.41/4.59 % Vampire exiting
%------------------------------------------------------------------------------