%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT360+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:19 AM UTC 2026
% Result : Theorem 25.37s 4.45s
% Output : Refutation 25.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 38
% Syntax : Number of formulae : 481 ( 43 unt; 20 def)
% Number of atoms : 3429 ( 40 equ)
% Maximal formula atoms : 32 ( 7 avg)
% Number of connectives : 5066 (2118 ~;2545 |; 286 &)
% ( 49 <=>; 68 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 17 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-3 aty)
% Number of variables : 667 ( 0 sgn 666 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_waybel34) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ~ v2_setfam_1(X0)
=> u1_struct_0(k4_waybel34(X0)) = u1_struct_0(k5_waybel34(X0)) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f37,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ~ v1_xboole_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc2_setfam_1) ).
fof(f47,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f48,axiom,
! [X0] :
( v2_setfam_1(X0)
<=> ! [X1] :
( ~ v1_xboole_0(X1)
=> ~ r2_hidden(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_setfam_1) ).
fof(f49,axiom,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X0)
=> r2_hidden(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(f50,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ ! [X1] :
( m1_subset_1(X1,X0)
=> v1_xboole_0(X1) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v11_altcat_1(X1)
& v12_altcat_1(X1)
& v2_yellow21(X1)
& l2_altcat_1(X1) )
=> ( X1 = k4_waybel34(X0)
<=> ( ! [X2] :
( ( v2_orders_2(X2)
& v3_orders_2(X2)
& v4_orders_2(X2)
& v1_lattice3(X2)
& v2_lattice3(X2)
& l1_orders_2(X2) )
=> ( m1_subset_1(X2,u1_struct_0(X1))
<=> ( v1_orders_2(X2)
& v3_lattice3(X2)
& r2_hidden(u1_struct_0(X2),X0) ) ) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(k3_yellow21(X1,X2)),u1_struct_0(k3_yellow21(X1,X3)))
& v5_orders_3(X4,k3_yellow21(X1,X2),k3_yellow21(X1,X3))
& m2_relset_1(X4,u1_struct_0(k3_yellow21(X1,X2)),u1_struct_0(k3_yellow21(X1,X3))) )
=> ( r2_hidden(X4,k1_altcat_1(X1,X2,X3))
<=> v17_waybel_0(X4,k3_yellow21(X1,X2),k3_yellow21(X1,X3)) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_waybel34) ).
fof(f51,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& l2_altcat_1(X0) )
=> ( v2_yellow21(X0)
<=> ( v9_altcat_1(X0)
& v3_yellow18(X0)
& ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) ) )
& ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( ( v2_orders_2(X3)
& v3_orders_2(X3)
& v4_orders_2(X3)
& v1_lattice3(X3)
& v2_lattice3(X3)
& l1_orders_2(X3) )
=> ! [X4] :
( ( v2_orders_2(X4)
& v3_orders_2(X4)
& v4_orders_2(X4)
& v1_lattice3(X4)
& v2_lattice3(X4)
& l1_orders_2(X4) )
=> ( ( X3 = X1
& X4 = X2 )
=> r1_tarski(k1_altcat_1(X0,X1,X2),k1_orders_3(X3,X4)) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_yellow21) ).
fof(f52,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ ! [X1] :
( m1_subset_1(X1,X0)
=> v1_xboole_0(X1) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v2_altcat_1(X1)
& v6_altcat_1(X1)
& v11_altcat_1(X1)
& v12_altcat_1(X1)
& v2_yellow21(X1)
& l2_altcat_1(X1) )
=> ( X1 = k5_waybel34(X0)
<=> ( ! [X2] :
( ( v2_orders_2(X2)
& v3_orders_2(X2)
& v4_orders_2(X2)
& v1_lattice3(X2)
& v2_lattice3(X2)
& l1_orders_2(X2) )
=> ( m1_subset_1(X2,u1_struct_0(X1))
<=> ( v1_orders_2(X2)
& v3_lattice3(X2)
& r2_hidden(u1_struct_0(X2),X0) ) ) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( ( v1_funct_1(X4)
& v1_funct_2(X4,u1_struct_0(k3_yellow21(X1,X2)),u1_struct_0(k3_yellow21(X1,X3)))
& v5_orders_3(X4,k3_yellow21(X1,X2),k3_yellow21(X1,X3))
& m2_relset_1(X4,u1_struct_0(k3_yellow21(X1,X2)),u1_struct_0(k3_yellow21(X1,X3))) )
=> ( r2_hidden(X4,k1_altcat_1(X1,X2,X3))
<=> v18_waybel_0(X4,k3_yellow21(X1,X2),k3_yellow21(X1,X3)) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_waybel34) ).
fof(f66,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k4_waybel34) ).
fof(f67,axiom,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel34) ).
fof(f68,axiom,
! [X0] :
( l1_altcat_1(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_altcat_1) ).
fof(f71,axiom,
! [X0] :
( l2_altcat_1(X0)
=> l1_altcat_1(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_altcat_1) ).
fof(f94,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f96,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v1_yellow21(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_waybel34) ).
fof(f99,axiom,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v1_yellow21(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_waybel34) ).
fof(f130,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f131,axiom,
! [X0,X1] :
( m1_subset_1(X0,X1)
=> ( v1_xboole_0(X1)
| r2_hidden(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f136,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f138,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ ! [X1] :
( m1_subset_1(X1,X0)
=> v1_xboole_0(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_altcat_1(X2)
& v6_altcat_1(X2)
& v11_altcat_1(X2)
& v12_altcat_1(X2)
& v2_yellow21(X2)
& l2_altcat_1(X2) )
=> ( k4_waybel34(X0) = X2
<=> ( ! [X3] :
( ( v2_orders_2(X3)
& v3_orders_2(X3)
& v4_orders_2(X3)
& v1_lattice3(X3)
& v2_lattice3(X3)
& l1_orders_2(X3) )
=> ( m1_subset_1(X3,u1_struct_0(X2))
<=> ( v1_orders_2(X3)
& v3_lattice3(X3)
& r2_hidden(u1_struct_0(X3),X0) ) ) )
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X2))
=> ! [X6] :
( ( v1_funct_1(X6)
& v1_funct_2(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5)))
& v5_orders_3(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5))
& m2_relset_1(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5))) )
=> ( r2_hidden(X6,k1_altcat_1(X2,X4,X5))
<=> v17_waybel_0(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5)) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f50]) ).
fof(f139,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_altcat_1(X0)
& v11_altcat_1(X0)
& v12_altcat_1(X0)
& l2_altcat_1(X0) )
=> ( v2_yellow21(X0)
<=> ( v9_altcat_1(X0)
& v3_yellow18(X0)
& ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) ) )
& ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ! [X4] :
( ( v2_orders_2(X4)
& v3_orders_2(X4)
& v4_orders_2(X4)
& v1_lattice3(X4)
& v2_lattice3(X4)
& l1_orders_2(X4) )
=> ! [X5] :
( ( v2_orders_2(X5)
& v3_orders_2(X5)
& v4_orders_2(X5)
& v1_lattice3(X5)
& v2_lattice3(X5)
& l1_orders_2(X5) )
=> ( ( X2 = X4
& X3 = X5 )
=> r1_tarski(k1_altcat_1(X0,X2,X3),k1_orders_3(X4,X5)) ) ) ) ) ) ) ) ),
inference(rectify,[],[f51]) ).
fof(f140,plain,
! [X0] :
( ~ v1_xboole_0(X0)
=> ( ~ ! [X1] :
( m1_subset_1(X1,X0)
=> v1_xboole_0(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v2_altcat_1(X2)
& v6_altcat_1(X2)
& v11_altcat_1(X2)
& v12_altcat_1(X2)
& v2_yellow21(X2)
& l2_altcat_1(X2) )
=> ( k5_waybel34(X0) = X2
<=> ( ! [X3] :
( ( v2_orders_2(X3)
& v3_orders_2(X3)
& v4_orders_2(X3)
& v1_lattice3(X3)
& v2_lattice3(X3)
& l1_orders_2(X3) )
=> ( m1_subset_1(X3,u1_struct_0(X2))
<=> ( v1_orders_2(X3)
& v3_lattice3(X3)
& r2_hidden(u1_struct_0(X3),X0) ) ) )
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X2))
=> ! [X6] :
( ( v1_funct_1(X6)
& v1_funct_2(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5)))
& v5_orders_3(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5))
& m2_relset_1(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5))) )
=> ( r2_hidden(X6,k1_altcat_1(X2,X4,X5))
<=> v18_waybel_0(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5)) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f52]) ).
fof(f147,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v4_yellow18(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f99]) ).
fof(f150,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v4_yellow18(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f96]) ).
fof(f152,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v2_yellow18(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f150]) ).
fof(f154,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v2_yellow18(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f147]) ).
fof(f155,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v1_altcat_2(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f152]) ).
fof(f156,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v1_altcat_2(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f154]) ).
fof(f162,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f156]) ).
fof(f167,plain,
! [X0] :
( ~ v2_setfam_1(X0)
=> ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) ) ),
inference(pure_predicate_removal,[],[f155]) ).
fof(f187,plain,
? [X0] :
( u1_struct_0(k4_waybel34(X0)) != u1_struct_0(k5_waybel34(X0))
& ~ v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f233,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f250,plain,
! [X0] :
( v2_setfam_1(X0)
<=> ! [X1] :
( ~ r2_hidden(X1,X0)
| v1_xboole_0(X1) ) ),
inference(ennf_transformation,[],[f48]) ).
fof(f251,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
<=> ! [X2] :
( r2_hidden(X2,X1)
| ~ r2_hidden(X2,X0) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f252,plain,
! [X0] :
( ! [X2] :
( ( k4_waybel34(X0) = X2
<=> ( ! [X3] :
( ( m1_subset_1(X3,u1_struct_0(X2))
<=> ( v1_orders_2(X3)
& v3_lattice3(X3)
& r2_hidden(u1_struct_0(X3),X0) ) )
| ~ v2_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v4_orders_2(X3)
| ~ v1_lattice3(X3)
| ~ v2_lattice3(X3)
| ~ l1_orders_2(X3) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( ( r2_hidden(X6,k1_altcat_1(X2,X4,X5))
<=> v17_waybel_0(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5)) )
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5)))
| ~ v5_orders_3(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5))
| ~ m2_relset_1(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5))) )
| ~ m1_subset_1(X5,u1_struct_0(X2)) )
| ~ m1_subset_1(X4,u1_struct_0(X2)) ) ) )
| v3_struct_0(X2)
| ~ v2_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v12_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ l2_altcat_1(X2) )
| ! [X1] :
( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f138]) ).
fof(f253,plain,
! [X0] :
( ! [X2] :
( ( k4_waybel34(X0) = X2
<=> ( ! [X3] :
( ( m1_subset_1(X3,u1_struct_0(X2))
<=> ( v1_orders_2(X3)
& v3_lattice3(X3)
& r2_hidden(u1_struct_0(X3),X0) ) )
| ~ v2_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v4_orders_2(X3)
| ~ v1_lattice3(X3)
| ~ v2_lattice3(X3)
| ~ l1_orders_2(X3) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( ( r2_hidden(X6,k1_altcat_1(X2,X4,X5))
<=> v17_waybel_0(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5)) )
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5)))
| ~ v5_orders_3(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5))
| ~ m2_relset_1(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5))) )
| ~ m1_subset_1(X5,u1_struct_0(X2)) )
| ~ m1_subset_1(X4,u1_struct_0(X2)) ) ) )
| v3_struct_0(X2)
| ~ v2_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v12_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ l2_altcat_1(X2) )
| ! [X1] :
( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f252]) ).
fof(f254,plain,
! [X0] :
( ( v2_yellow21(X0)
<=> ( v9_altcat_1(X0)
& v3_yellow18(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
& ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r1_tarski(k1_altcat_1(X0,X2,X3),k1_orders_3(X4,X5))
| X2 != X4
| X3 != X5
| ~ v2_orders_2(X5)
| ~ v3_orders_2(X5)
| ~ v4_orders_2(X5)
| ~ v1_lattice3(X5)
| ~ v2_lattice3(X5)
| ~ l1_orders_2(X5) )
| ~ v2_orders_2(X4)
| ~ v3_orders_2(X4)
| ~ v4_orders_2(X4)
| ~ v1_lattice3(X4)
| ~ v2_lattice3(X4)
| ~ l1_orders_2(X4) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f139]) ).
fof(f255,plain,
! [X0] :
( ( v2_yellow21(X0)
<=> ( v9_altcat_1(X0)
& v3_yellow18(X0)
& ! [X1] :
( ( v2_orders_2(X1)
& v3_orders_2(X1)
& v4_orders_2(X1)
& v1_lattice3(X1)
& v2_lattice3(X1)
& l1_orders_2(X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
& ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( r1_tarski(k1_altcat_1(X0,X2,X3),k1_orders_3(X4,X5))
| X2 != X4
| X3 != X5
| ~ v2_orders_2(X5)
| ~ v3_orders_2(X5)
| ~ v4_orders_2(X5)
| ~ v1_lattice3(X5)
| ~ v2_lattice3(X5)
| ~ l1_orders_2(X5) )
| ~ v2_orders_2(X4)
| ~ v3_orders_2(X4)
| ~ v4_orders_2(X4)
| ~ v1_lattice3(X4)
| ~ v2_lattice3(X4)
| ~ l1_orders_2(X4) )
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ m1_subset_1(X2,u1_struct_0(X0)) ) ) )
| v3_struct_0(X0)
| ~ v2_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v12_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(flattening,[],[f254]) ).
fof(f256,plain,
! [X0] :
( ! [X2] :
( ( k5_waybel34(X0) = X2
<=> ( ! [X3] :
( ( m1_subset_1(X3,u1_struct_0(X2))
<=> ( v1_orders_2(X3)
& v3_lattice3(X3)
& r2_hidden(u1_struct_0(X3),X0) ) )
| ~ v2_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v4_orders_2(X3)
| ~ v1_lattice3(X3)
| ~ v2_lattice3(X3)
| ~ l1_orders_2(X3) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( ( r2_hidden(X6,k1_altcat_1(X2,X4,X5))
<=> v18_waybel_0(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5)) )
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5)))
| ~ v5_orders_3(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5))
| ~ m2_relset_1(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5))) )
| ~ m1_subset_1(X5,u1_struct_0(X2)) )
| ~ m1_subset_1(X4,u1_struct_0(X2)) ) ) )
| v3_struct_0(X2)
| ~ v2_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v12_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ l2_altcat_1(X2) )
| ! [X1] :
( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f257,plain,
! [X0] :
( ! [X2] :
( ( k5_waybel34(X0) = X2
<=> ( ! [X3] :
( ( m1_subset_1(X3,u1_struct_0(X2))
<=> ( v1_orders_2(X3)
& v3_lattice3(X3)
& r2_hidden(u1_struct_0(X3),X0) ) )
| ~ v2_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v4_orders_2(X3)
| ~ v1_lattice3(X3)
| ~ v2_lattice3(X3)
| ~ l1_orders_2(X3) )
& ! [X4] :
( ! [X5] :
( ! [X6] :
( ( r2_hidden(X6,k1_altcat_1(X2,X4,X5))
<=> v18_waybel_0(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5)) )
| ~ v1_funct_1(X6)
| ~ v1_funct_2(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5)))
| ~ v5_orders_3(X6,k3_yellow21(X2,X4),k3_yellow21(X2,X5))
| ~ m2_relset_1(X6,u1_struct_0(k3_yellow21(X2,X4)),u1_struct_0(k3_yellow21(X2,X5))) )
| ~ m1_subset_1(X5,u1_struct_0(X2)) )
| ~ m1_subset_1(X4,u1_struct_0(X2)) ) ) )
| v3_struct_0(X2)
| ~ v2_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v12_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ l2_altcat_1(X2) )
| ! [X1] :
( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) )
| v1_xboole_0(X0) ),
inference(flattening,[],[f256]) ).
fof(f268,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& l2_altcat_1(k4_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f66]) ).
fof(f269,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& l2_altcat_1(k5_waybel34(X0)) )
| v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f270,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_altcat_1(X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f272,plain,
! [X0] :
( l1_altcat_1(X0)
| ~ l2_altcat_1(X0) ),
inference(ennf_transformation,[],[f71]) ).
fof(f290,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f291,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f290]) ).
fof(f294,plain,
! [X0] :
( ( ~ v3_struct_0(k4_waybel34(X0))
& v2_altcat_1(k4_waybel34(X0))
& v6_altcat_1(k4_waybel34(X0))
& v9_altcat_1(k4_waybel34(X0))
& v11_altcat_1(k4_waybel34(X0))
& v12_altcat_1(k4_waybel34(X0))
& v3_yellow18(k4_waybel34(X0))
& v2_yellow21(k4_waybel34(X0))
& v3_yellow21(k4_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f167]) ).
fof(f297,plain,
! [X0] :
( ( ~ v3_struct_0(k5_waybel34(X0))
& v2_altcat_1(k5_waybel34(X0))
& v6_altcat_1(k5_waybel34(X0))
& v9_altcat_1(k5_waybel34(X0))
& v11_altcat_1(k5_waybel34(X0))
& v12_altcat_1(k5_waybel34(X0))
& v3_yellow18(k5_waybel34(X0))
& v2_yellow21(k5_waybel34(X0))
& v3_yellow21(k5_waybel34(X0)) )
| v2_setfam_1(X0) ),
inference(ennf_transformation,[],[f162]) ).
fof(f324,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f130]) ).
fof(f325,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(ennf_transformation,[],[f131]) ).
fof(f326,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| r2_hidden(X0,X1)
| ~ m1_subset_1(X0,X1) ),
inference(flattening,[],[f325]) ).
fof(f331,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f136]) ).
fof(f333,plain,
~ v2_setfam_1(sK0),
inference(cnf_transformation,[],[f187]) ).
fof(f334,plain,
u1_struct_0(k4_waybel34(sK0)) != u1_struct_0(k5_waybel34(sK0)),
inference(cnf_transformation,[],[f187]) ).
fof(f386,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f233]) ).
fof(f401,plain,
! [X0,X1] :
( ~ r1_tarski(X1,X0)
| ~ r1_tarski(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f47]) ).
fof(f403,plain,
! [X0] :
( ~ v1_xboole_0(sK1(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f404,plain,
! [X0] :
( r2_hidden(sK1(X0),X0)
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f250]) ).
fof(f406,plain,
! [X0,X1] :
( r2_hidden(sK2(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f251]) ).
fof(f407,plain,
! [X0,X1] :
( ~ r2_hidden(sK2(X0,X1),X1)
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f251]) ).
fof(f417,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k4_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f253]) ).
fof(f418,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k4_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f253]) ).
fof(f419,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k4_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f253]) ).
fof(f420,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| ~ r2_hidden(u1_struct_0(X3),X0)
| ~ v3_lattice3(X3)
| ~ v1_orders_2(X3)
| m1_subset_1(X3,u1_struct_0(X2))
| k4_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f253]) ).
fof(f476,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| l1_orders_2(X1)
| ~ v2_yellow21(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f477,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| v2_lattice3(X1)
| ~ v2_yellow21(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f478,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| v1_lattice3(X1)
| ~ v2_yellow21(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f479,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| v4_orders_2(X1)
| ~ v2_yellow21(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f480,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| v3_orders_2(X1)
| ~ v2_yellow21(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f481,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v12_altcat_1(X0)
| ~ v11_altcat_1(X0)
| ~ v2_altcat_1(X0)
| v3_struct_0(X0)
| ~ l2_altcat_1(X0)
| v2_orders_2(X1)
| ~ v2_yellow21(X0) ),
inference(cnf_transformation,[],[f255]) ).
fof(f494,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k5_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f257]) ).
fof(f495,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k5_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f257]) ).
fof(f496,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| k5_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f257]) ).
fof(f497,plain,
! [X2,X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(X2)
| ~ v2_yellow21(X2)
| ~ v12_altcat_1(X2)
| ~ v11_altcat_1(X2)
| ~ v6_altcat_1(X2)
| ~ v2_altcat_1(X2)
| v3_struct_0(X2)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| ~ r2_hidden(u1_struct_0(X3),X0)
| ~ v3_lattice3(X3)
| ~ v1_orders_2(X3)
| m1_subset_1(X3,u1_struct_0(X2))
| k5_waybel34(X0) != X2 ),
inference(cnf_transformation,[],[f257]) ).
fof(f533,plain,
! [X0] :
( l2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f534,plain,
! [X0] :
( v2_yellow21(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f535,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f536,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f537,plain,
! [X0] :
( v6_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f538,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f539,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f268]) ).
fof(f540,plain,
! [X0] :
( l2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f541,plain,
! [X0] :
( v2_yellow21(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f542,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f543,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f544,plain,
! [X0] :
( v6_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f545,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f546,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f269]) ).
fof(f547,plain,
! [X0] :
( ~ l1_altcat_1(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f270]) ).
fof(f549,plain,
! [X0] :
( ~ l2_altcat_1(X0)
| l1_altcat_1(X0) ),
inference(cnf_transformation,[],[f272]) ).
fof(f573,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f291]) ).
fof(f577,plain,
! [X0] :
( v2_yellow21(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f579,plain,
! [X0] :
( v12_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f580,plain,
! [X0] :
( v11_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f582,plain,
! [X0] :
( v6_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f583,plain,
! [X0] :
( v2_altcat_1(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f584,plain,
! [X0] :
( ~ v3_struct_0(k4_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f294]) ).
fof(f595,plain,
! [X0] :
( v2_yellow21(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f597,plain,
! [X0] :
( v12_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f598,plain,
! [X0] :
( v11_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f600,plain,
! [X0] :
( v6_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f601,plain,
! [X0] :
( v2_altcat_1(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f602,plain,
! [X0] :
( ~ v3_struct_0(k5_waybel34(X0))
| v2_setfam_1(X0) ),
inference(cnf_transformation,[],[f297]) ).
fof(f727,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f324]) ).
fof(f728,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,X1)
| r2_hidden(X0,X1)
| v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f326]) ).
fof(f734,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f331]) ).
fof(f739,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| ~ r2_hidden(u1_struct_0(X3),X0)
| ~ v3_lattice3(X3)
| ~ v1_orders_2(X3)
| m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(equality_resolution,[],[f420]) ).
fof(f740,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(equality_resolution,[],[f419]) ).
fof(f741,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(equality_resolution,[],[f418]) ).
fof(f742,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(equality_resolution,[],[f417]) ).
fof(f746,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| ~ r2_hidden(u1_struct_0(X3),X0)
| ~ v3_lattice3(X3)
| ~ v1_orders_2(X3)
| m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(equality_resolution,[],[f497]) ).
fof(f747,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(equality_resolution,[],[f496]) ).
fof(f748,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(equality_resolution,[],[f495]) ).
fof(f749,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(equality_resolution,[],[f494]) ).
fof(f750,definition,
sF48 = k4_waybel34(sK0),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f751,plain,
k4_waybel34(sK0) = sF48,
inference(reorient_equations,[],[f750]) ).
fof(f752,definition,
sF49 = u1_struct_0(sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f753,plain,
u1_struct_0(sF48) = sF49,
inference(reorient_equations,[],[f752]) ).
fof(f754,definition,
sF50 = k5_waybel34(sK0),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f755,plain,
k5_waybel34(sK0) = sF50,
inference(reorient_equations,[],[f754]) ).
fof(f756,definition,
sF51 = u1_struct_0(sF50),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f757,plain,
u1_struct_0(sF50) = sF51,
inference(reorient_equations,[],[f756]) ).
fof(f758,plain,
sF49 != sF51,
inference(definition_folding,[],[f334,f757,f755,f753,f751]) ).
fof(f759,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f749,f540]) ).
fof(f760,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f748,f540]) ).
fof(f761,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f747,f540]) ).
fof(f762,plain,
! [X3,X0,X1] :
( m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
| v1_xboole_0(X1)
| ~ l2_altcat_1(k5_waybel34(X0))
| ~ v2_yellow21(k5_waybel34(X0))
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| ~ r2_hidden(u1_struct_0(X3),X0)
| ~ v3_lattice3(X3)
| ~ v1_orders_2(X3)
| ~ m1_subset_1(X1,X0) ),
inference(forward_subsumption_resolution,[],[f746,f734]) ).
fof(f767,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f742,f476]) ).
fof(f768,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f741,f476]) ).
fof(f769,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f740,f476]) ).
fof(f770,plain,
! [X3,X0,X1] :
( m1_subset_1(X3,u1_struct_0(k4_waybel34(X0)))
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| ~ r2_hidden(u1_struct_0(X3),X0)
| ~ v3_lattice3(X3)
| ~ v1_orders_2(X3)
| ~ m1_subset_1(X1,X0) ),
inference(forward_subsumption_resolution,[],[f739,f734]) ).
fof(f778,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f759,f541]) ).
fof(f779,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f760,f541]) ).
fof(f780,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v12_altcat_1(k5_waybel34(X0))
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f761,f541]) ).
fof(f783,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f767,f477]) ).
fof(f784,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f768,f477]) ).
fof(f785,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f769,f477]) ).
fof(f787,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f778,f542]) ).
fof(f788,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f779,f542]) ).
fof(f789,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v11_altcat_1(k5_waybel34(X0))
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f780,f542]) ).
fof(f792,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f783,f478]) ).
fof(f793,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f784,f478]) ).
fof(f794,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f785,f478]) ).
fof(f796,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f787,f543]) ).
fof(f797,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f788,f543]) ).
fof(f798,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v6_altcat_1(k5_waybel34(X0))
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f789,f543]) ).
fof(f801,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f792,f479]) ).
fof(f802,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f793,f479]) ).
fof(f803,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f794,f479]) ).
fof(f805,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f796,f544]) ).
fof(f806,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f797,f544]) ).
fof(f807,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_altcat_1(k5_waybel34(X0))
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f798,f544]) ).
fof(f810,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f801,f480]) ).
fof(f811,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f802,f480]) ).
fof(f812,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f803,f480]) ).
fof(f814,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f805,f545]) ).
fof(f815,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f806,f545]) ).
fof(f816,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_struct_0(k5_waybel34(X0))
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f807,f545]) ).
fof(f819,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f810,f481]) ).
fof(f820,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f811,f481]) ).
fof(f821,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_altcat_1(k4_waybel34(X0))
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f812,f481]) ).
fof(f823,plain,
! [X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| r2_hidden(u1_struct_0(X3),X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f814,f546]) ).
fof(f824,plain,
! [X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v3_lattice3(X3)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f815,f546]) ).
fof(f825,plain,
! [X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k5_waybel34(X0)))
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X3)
| ~ v2_lattice3(X3)
| ~ v1_lattice3(X3)
| ~ v4_orders_2(X3)
| ~ v3_orders_2(X3)
| ~ v2_orders_2(X3)
| v1_orders_2(X3)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f816,f546]) ).
fof(f828,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f819,f533]) ).
fof(f829,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f820,f533]) ).
fof(f830,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_yellow21(k4_waybel34(X0))
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f821,f533]) ).
fof(f833,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f828,f534]) ).
fof(f834,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f829,f534]) ).
fof(f835,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v12_altcat_1(k4_waybel34(X0))
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f830,f534]) ).
fof(f837,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f833,f535]) ).
fof(f838,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f834,f535]) ).
fof(f839,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v11_altcat_1(k4_waybel34(X0))
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f835,f535]) ).
fof(f841,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f837,f536]) ).
fof(f842,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f838,f536]) ).
fof(f843,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v6_altcat_1(k4_waybel34(X0))
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f839,f536]) ).
fof(f845,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f841,f537]) ).
fof(f846,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f842,f537]) ).
fof(f847,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| ~ v2_altcat_1(k4_waybel34(X0))
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f843,f537]) ).
fof(f849,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_struct_0(k4_waybel34(X0))
| r2_hidden(u1_struct_0(X3),X0)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f845,f538]) ).
fof(f850,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_struct_0(k4_waybel34(X0))
| v3_lattice3(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f846,f538]) ).
fof(f851,plain,
! [X3,X0,X1] :
( v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_struct_0(k4_waybel34(X0))
| v1_orders_2(X3)
| ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0))) ),
inference(forward_subsumption_resolution,[],[f847,f538]) ).
fof(f852,plain,
! [X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0)))
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| r2_hidden(u1_struct_0(X3),X0)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f849,f539]) ).
fof(f853,plain,
! [X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0)))
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v3_lattice3(X3)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f850,f539]) ).
fof(f854,plain,
! [X3,X0,X1] :
( ~ m1_subset_1(X3,u1_struct_0(k4_waybel34(X0)))
| ~ m1_subset_1(X1,X0)
| v1_xboole_0(X1)
| v1_orders_2(X3)
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[],[f851,f539]) ).
fof(f856,plain,
( ~ v3_struct_0(sF48)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f584,f751]) ).
fof(f857,plain,
~ v3_struct_0(sF48),
inference(forward_subsumption_resolution,[],[f856,f333]) ).
fof(f858,plain,
( ~ v3_struct_0(sF50)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f602,f755]) ).
fof(f859,plain,
~ v3_struct_0(sF50),
inference(forward_subsumption_resolution,[],[f858,f333]) ).
fof(f861,plain,
( v11_altcat_1(sF48)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f580,f751]) ).
fof(f862,plain,
v11_altcat_1(sF48),
inference(forward_subsumption_resolution,[],[f861,f333]) ).
fof(f863,plain,
( v2_yellow21(sF48)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f577,f751]) ).
fof(f864,plain,
v2_yellow21(sF48),
inference(forward_subsumption_resolution,[],[f863,f333]) ).
fof(f865,plain,
( v11_altcat_1(sF50)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f598,f755]) ).
fof(f866,plain,
v11_altcat_1(sF50),
inference(forward_subsumption_resolution,[],[f865,f333]) ).
fof(f867,plain,
( v2_yellow21(sF50)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f595,f755]) ).
fof(f868,plain,
v2_yellow21(sF50),
inference(forward_subsumption_resolution,[],[f867,f333]) ).
fof(f869,plain,
( v6_altcat_1(sF48)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f582,f751]) ).
fof(f870,plain,
v6_altcat_1(sF48),
inference(forward_subsumption_resolution,[],[f869,f333]) ).
fof(f871,plain,
( v6_altcat_1(sF50)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f600,f755]) ).
fof(f872,plain,
v6_altcat_1(sF50),
inference(forward_subsumption_resolution,[],[f871,f333]) ).
fof(f873,plain,
( v2_altcat_1(sF48)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f583,f751]) ).
fof(f874,plain,
v2_altcat_1(sF48),
inference(forward_subsumption_resolution,[],[f873,f333]) ).
fof(f875,plain,
( v12_altcat_1(sF48)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f579,f751]) ).
fof(f876,plain,
v12_altcat_1(sF48),
inference(forward_subsumption_resolution,[],[f875,f333]) ).
fof(f877,plain,
( v2_altcat_1(sF50)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f601,f755]) ).
fof(f878,plain,
v2_altcat_1(sF50),
inference(forward_subsumption_resolution,[],[f877,f333]) ).
fof(f879,plain,
( v12_altcat_1(sF50)
| v2_setfam_1(sK0) ),
inference(superposition,[],[f597,f755]) ).
fof(f880,plain,
v12_altcat_1(sF50),
inference(forward_subsumption_resolution,[],[f879,f333]) ).
fof(f881,plain,
( l2_altcat_1(sF48)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f533,f751]) ).
fof(f883,definition,
( spl52_1
<=> v1_xboole_0(sK0) ),
introduced(definition,[new_symbols(definition,[spl52_1])],[avatar_definition]) ).
fof(f884,plain,
( v1_xboole_0(sK0)
| ~ spl52_1 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f886,definition,
( spl52_2
<=> l2_altcat_1(sF48) ),
introduced(definition,[new_symbols(definition,[spl52_2])],[avatar_definition]) ).
fof(f887,plain,
( l2_altcat_1(sF48)
| ~ spl52_2 ),
inference(avatar_component_clause,[],[f886]) ).
fof(f888,plain,
( spl52_1
| spl52_2 ),
inference(avatar_split_clause,[],[f881,f886,f883]) ).
fof(f889,plain,
( l2_altcat_1(sF50)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f540,f755]) ).
fof(f891,definition,
( spl52_3
<=> l2_altcat_1(sF50) ),
introduced(definition,[new_symbols(definition,[spl52_3])],[avatar_definition]) ).
fof(f892,plain,
( l2_altcat_1(sF50)
| ~ spl52_3 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f893,plain,
( spl52_1
| spl52_3 ),
inference(avatar_split_clause,[],[f889,f891,f883]) ).
fof(f896,plain,
( v2_setfam_1(sK0)
| ~ spl52_1 ),
inference(resolution,[],[f386,f884]) ).
fof(f898,plain,
( $false
| ~ spl52_1 ),
inference(forward_subsumption_resolution,[],[f896,f333]) ).
fof(f899,plain,
~ spl52_1,
inference(avatar_contradiction_clause,[],[f898]) ).
fof(f904,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| r2_hidden(u1_struct_0(X0),sK0)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f852,f751]) ).
fof(f905,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF49)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| r2_hidden(u1_struct_0(X0),sK0)
| v1_xboole_0(sK0) ),
inference(forward_demodulation,[],[f904,f753]) ).
fof(f907,definition,
( spl52_5
<=> ! [X1] :
( ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl52_5])],[avatar_definition]) ).
fof(f908,plain,
( ! [X1] :
( ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1) )
| ~ spl52_5 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f910,definition,
( spl52_6
<=> ! [X0] :
( ~ m1_subset_1(X0,sF49)
| r2_hidden(u1_struct_0(X0),sK0) ) ),
introduced(definition,[new_symbols(definition,[spl52_6])],[avatar_definition]) ).
fof(f911,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_6 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f912,plain,
( spl52_1
| spl52_5
| spl52_6 ),
inference(avatar_split_clause,[],[f905,f910,f907,f883]) ).
fof(f945,plain,
( ~ v1_xboole_0(sF49)
| v3_struct_0(sF48)
| ~ l1_struct_0(sF48) ),
inference(superposition,[],[f573,f753]) ).
fof(f946,plain,
( ~ v1_xboole_0(sF51)
| v3_struct_0(sF50)
| ~ l1_struct_0(sF50) ),
inference(superposition,[],[f573,f757]) ).
fof(f947,plain,
( ~ v1_xboole_0(sF51)
| ~ l1_struct_0(sF50) ),
inference(forward_subsumption_resolution,[],[f946,f859]) ).
fof(f948,plain,
( ~ v1_xboole_0(sF49)
| ~ l1_struct_0(sF48) ),
inference(forward_subsumption_resolution,[],[f945,f857]) ).
fof(f951,plain,
( l1_altcat_1(sF48)
| ~ spl52_2 ),
inference(resolution,[],[f549,f887]) ).
fof(f952,plain,
( l1_altcat_1(sF50)
| ~ spl52_3 ),
inference(resolution,[],[f549,f892]) ).
fof(f953,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v3_lattice3(X0)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f853,f751]) ).
fof(f954,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v1_orders_2(X0)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f854,f751]) ).
fof(f956,definition,
( spl52_8
<=> l1_struct_0(sF48) ),
introduced(definition,[new_symbols(definition,[spl52_8])],[avatar_definition]) ).
fof(f957,plain,
( ~ l1_struct_0(sF48)
| spl52_8 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f959,definition,
( spl52_9
<=> v1_xboole_0(sF49) ),
introduced(definition,[new_symbols(definition,[spl52_9])],[avatar_definition]) ).
fof(f960,plain,
( ~ v1_xboole_0(sF49)
| spl52_9 ),
inference(avatar_component_clause,[],[f959]) ).
fof(f961,plain,
( ~ spl52_8
| ~ spl52_9 ),
inference(avatar_split_clause,[],[f948,f959,f956]) ).
fof(f963,definition,
( spl52_10
<=> l1_struct_0(sF50) ),
introduced(definition,[new_symbols(definition,[spl52_10])],[avatar_definition]) ).
fof(f964,plain,
( ~ l1_struct_0(sF50)
| spl52_10 ),
inference(avatar_component_clause,[],[f963]) ).
fof(f966,definition,
( spl52_11
<=> v1_xboole_0(sF51) ),
introduced(definition,[new_symbols(definition,[spl52_11])],[avatar_definition]) ).
fof(f967,plain,
( ~ v1_xboole_0(sF51)
| spl52_11 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f968,plain,
( ~ spl52_10
| ~ spl52_11 ),
inference(avatar_split_clause,[],[f947,f966,f963]) ).
fof(f969,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF50))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f823,f755]) ).
fof(f993,plain,
! [X0] :
( m1_subset_1(sK1(X0),X0)
| v2_setfam_1(X0) ),
inference(resolution,[],[f404,f727]) ).
fof(f1002,plain,
( l1_struct_0(sF48)
| ~ spl52_2 ),
inference(resolution,[],[f547,f951]) ).
fof(f1003,plain,
( l1_struct_0(sF50)
| ~ spl52_3 ),
inference(resolution,[],[f547,f952]) ).
fof(f1006,plain,
( $false
| ~ spl52_3
| spl52_10 ),
inference(forward_subsumption_resolution,[],[f1003,f964]) ).
fof(f1007,plain,
( ~ spl52_3
| spl52_10 ),
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1008,plain,
( $false
| ~ spl52_2
| spl52_8 ),
inference(forward_subsumption_resolution,[],[f1002,f957]) ).
fof(f1009,plain,
( ~ spl52_2
| spl52_8 ),
inference(avatar_contradiction_clause,[],[f1008]) ).
fof(f1209,plain,
( ~ v1_xboole_0(sK0)
| spl52_1 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f1380,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF50))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f824,f755]) ).
fof(f1403,plain,
! [X0,X1] :
( m1_subset_1(sK2(X0,X1),X0)
| r1_tarski(X0,X1) ),
inference(resolution,[],[f406,f727]) ).
fof(f1405,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF50))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0)
| v1_xboole_0(sK0) ),
inference(superposition,[],[f825,f755]) ).
fof(f1406,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| l1_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(superposition,[],[f476,f753]) ).
fof(f1407,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| l1_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(superposition,[],[f476,f757]) ).
fof(f1409,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| l1_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1407,f880]) ).
fof(f1410,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| l1_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1406,f876]) ).
fof(f1411,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| l1_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1409,f866]) ).
fof(f1412,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| l1_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1410,f862]) ).
fof(f1413,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| l1_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1411,f878]) ).
fof(f1414,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| l1_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1412,f874]) ).
fof(f1415,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ l2_altcat_1(sF50)
| l1_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1413,f859]) ).
fof(f1416,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ l2_altcat_1(sF48)
| l1_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1414,f857]) ).
fof(f1417,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| l1_orders_2(X0)
| ~ v2_yellow21(sF50) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1415,f892]) ).
fof(f1418,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| l1_orders_2(X0)
| ~ v2_yellow21(sF48) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1416,f887]) ).
fof(f1419,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| l1_orders_2(X0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1417,f868]) ).
fof(f1420,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| l1_orders_2(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1418,f864]) ).
fof(f1434,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(superposition,[],[f481,f753]) ).
fof(f1435,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(superposition,[],[f481,f757]) ).
fof(f1437,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1435,f880]) ).
fof(f1438,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1434,f876]) ).
fof(f1439,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1437,f866]) ).
fof(f1440,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1438,f862]) ).
fof(f1441,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1439,f878]) ).
fof(f1442,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1440,f874]) ).
fof(f1443,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ l2_altcat_1(sF50)
| v2_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1441,f859]) ).
fof(f1444,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ l2_altcat_1(sF48)
| v2_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1442,f857]) ).
fof(f1445,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v2_orders_2(X0)
| ~ v2_yellow21(sF50) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1443,f892]) ).
fof(f1446,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v2_orders_2(X0)
| ~ v2_yellow21(sF48) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1444,f887]) ).
fof(f1447,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v2_orders_2(X0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1445,f868]) ).
fof(f1448,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v2_orders_2(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1446,f864]) ).
fof(f1487,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v3_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(superposition,[],[f480,f753]) ).
fof(f1488,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v3_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(superposition,[],[f480,f757]) ).
fof(f1490,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v3_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1488,f880]) ).
fof(f1491,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v3_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1487,f876]) ).
fof(f1492,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v3_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1490,f866]) ).
fof(f1493,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v3_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1491,f862]) ).
fof(f1494,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v3_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1492,f878]) ).
fof(f1495,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v3_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1493,f874]) ).
fof(f1496,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ l2_altcat_1(sF50)
| v3_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1494,f859]) ).
fof(f1497,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ l2_altcat_1(sF48)
| v3_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1495,f857]) ).
fof(f1498,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_orders_2(X0)
| ~ v2_yellow21(sF50) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1496,f892]) ).
fof(f1499,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_orders_2(X0)
| ~ v2_yellow21(sF48) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1497,f887]) ).
fof(f1500,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_orders_2(X0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1498,f868]) ).
fof(f1501,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_orders_2(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1499,f864]) ).
fof(f1505,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(superposition,[],[f477,f753]) ).
fof(f1506,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(superposition,[],[f477,f757]) ).
fof(f1508,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1506,f880]) ).
fof(f1509,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1505,f876]) ).
fof(f1510,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1508,f866]) ).
fof(f1511,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1509,f862]) ).
fof(f1512,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v2_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1510,f878]) ).
fof(f1513,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v2_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1511,f874]) ).
fof(f1514,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ l2_altcat_1(sF50)
| v2_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1512,f859]) ).
fof(f1515,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ l2_altcat_1(sF48)
| v2_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1513,f857]) ).
fof(f1516,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v2_lattice3(X0)
| ~ v2_yellow21(sF50) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1514,f892]) ).
fof(f1517,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v2_lattice3(X0)
| ~ v2_yellow21(sF48) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1515,f887]) ).
fof(f1518,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v2_lattice3(X0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1516,f868]) ).
fof(f1519,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v2_lattice3(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1517,f864]) ).
fof(f1531,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v4_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(superposition,[],[f479,f753]) ).
fof(f1532,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v4_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(superposition,[],[f479,f757]) ).
fof(f1534,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v4_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1532,f880]) ).
fof(f1535,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v4_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1531,f876]) ).
fof(f1536,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v4_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1534,f866]) ).
fof(f1537,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v4_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1535,f862]) ).
fof(f1538,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v4_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1536,f878]) ).
fof(f1539,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v4_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1537,f874]) ).
fof(f1540,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ l2_altcat_1(sF50)
| v4_orders_2(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1538,f859]) ).
fof(f1541,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ l2_altcat_1(sF48)
| v4_orders_2(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1539,f857]) ).
fof(f1542,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v4_orders_2(X0)
| ~ v2_yellow21(sF50) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1540,f892]) ).
fof(f1543,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v4_orders_2(X0)
| ~ v2_yellow21(sF48) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1541,f887]) ).
fof(f1544,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v4_orders_2(X0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1542,f868]) ).
fof(f1545,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v4_orders_2(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1543,f864]) ).
fof(f1552,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v1_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(superposition,[],[f478,f753]) ).
fof(f1553,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v1_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(superposition,[],[f478,f757]) ).
fof(f1555,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v11_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v1_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1553,f880]) ).
fof(f1556,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v11_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v1_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1552,f876]) ).
fof(f1557,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v1_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1555,f866]) ).
fof(f1558,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v1_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1556,f862]) ).
fof(f1559,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_struct_0(sF50)
| ~ l2_altcat_1(sF50)
| v1_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1557,f878]) ).
fof(f1560,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_struct_0(sF48)
| ~ l2_altcat_1(sF48)
| v1_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1558,f874]) ).
fof(f1561,plain,
! [X0] :
( ~ m1_subset_1(X0,sF51)
| ~ l2_altcat_1(sF50)
| v1_lattice3(X0)
| ~ v2_yellow21(sF50) ),
inference(forward_subsumption_resolution,[],[f1559,f859]) ).
fof(f1562,plain,
! [X0] :
( ~ m1_subset_1(X0,sF49)
| ~ l2_altcat_1(sF48)
| v1_lattice3(X0)
| ~ v2_yellow21(sF48) ),
inference(forward_subsumption_resolution,[],[f1560,f857]) ).
fof(f1563,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v1_lattice3(X0)
| ~ v2_yellow21(sF50) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1561,f892]) ).
fof(f1564,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v1_lattice3(X0)
| ~ v2_yellow21(sF48) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1562,f887]) ).
fof(f1565,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v1_lattice3(X0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f1563,f868]) ).
fof(f1566,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v1_lattice3(X0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f1564,f864]) ).
fof(f2042,plain,
( v2_setfam_1(sK0)
| v1_xboole_0(sK1(sK0))
| ~ spl52_5 ),
inference(resolution,[],[f993,f908]) ).
fof(f2070,plain,
( v1_xboole_0(sK1(sK0))
| ~ spl52_5 ),
inference(forward_subsumption_resolution,[],[f2042,f333]) ).
fof(f2072,plain,
( v2_setfam_1(sK0)
| ~ spl52_5 ),
inference(resolution,[],[f2070,f403]) ).
fof(f2075,plain,
( $false
| ~ spl52_5 ),
inference(forward_subsumption_resolution,[],[f2072,f333]) ).
fof(f2076,plain,
~ spl52_5,
inference(avatar_contradiction_clause,[],[f2075]) ).
fof(f2078,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v3_lattice3(X0) )
| spl52_1 ),
inference(forward_subsumption_resolution,[],[f953,f1209]) ).
fof(f2079,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF48))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v1_orders_2(X0) )
| spl52_1 ),
inference(forward_subsumption_resolution,[],[f954,f1209]) ).
fof(f2080,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF50))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1 ),
inference(forward_subsumption_resolution,[],[f969,f1209]) ).
fof(f2081,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF50))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1 ),
inference(forward_subsumption_resolution,[],[f1380,f1209]) ).
fof(f2082,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(sF50))
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1 ),
inference(forward_subsumption_resolution,[],[f1405,f1209]) ).
fof(f2088,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF49)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v3_lattice3(X0) )
| spl52_1 ),
inference(forward_demodulation,[],[f2078,f753]) ).
fof(f2089,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF49)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v1_orders_2(X0) )
| spl52_1 ),
inference(forward_demodulation,[],[f2079,f753]) ).
fof(f2090,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1 ),
inference(forward_demodulation,[],[f2080,f757]) ).
fof(f2091,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1 ),
inference(forward_demodulation,[],[f2081,f757]) ).
fof(f2092,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1 ),
inference(forward_demodulation,[],[f2082,f757]) ).
fof(f2097,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2090,f1419]) ).
fof(f2098,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2091,f1419]) ).
fof(f2099,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2092,f1419]) ).
fof(f2102,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2097,f1518]) ).
fof(f2103,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2098,f1518]) ).
fof(f2104,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2099,f1518]) ).
fof(f2105,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2102,f1565]) ).
fof(f2106,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2103,f1565]) ).
fof(f2107,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2104,f1565]) ).
fof(f2108,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2105,f1544]) ).
fof(f2109,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2106,f1544]) ).
fof(f2110,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2107,f1544]) ).
fof(f2111,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v2_orders_2(X0)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2108,f1500]) ).
fof(f2112,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v2_orders_2(X0)
| v3_lattice3(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2109,f1500]) ).
fof(f2113,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| ~ v2_orders_2(X0)
| v1_orders_2(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2110,f1500]) ).
fof(f2114,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| r2_hidden(u1_struct_0(X0),sK0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2111,f1447]) ).
fof(f2115,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v3_lattice3(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2112,f1447]) ).
fof(f2116,plain,
( ! [X0,X1] :
( ~ m1_subset_1(X0,sF51)
| ~ m1_subset_1(X1,sK0)
| v1_xboole_0(X1)
| v1_orders_2(X0) )
| spl52_1
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2113,f1447]) ).
fof(f2122,definition,
( spl52_36
<=> ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_lattice3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_36])],[avatar_definition]) ).
fof(f2123,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v3_lattice3(X0) )
| ~ spl52_36 ),
inference(avatar_component_clause,[],[f2122]) ).
fof(f2124,plain,
( spl52_5
| spl52_36
| spl52_1 ),
inference(avatar_split_clause,[],[f2088,f883,f2122,f907]) ).
fof(f2130,definition,
( spl52_37
<=> ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_37])],[avatar_definition]) ).
fof(f2131,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| v1_orders_2(X0) )
| ~ spl52_37 ),
inference(avatar_component_clause,[],[f2130]) ).
fof(f2132,plain,
( spl52_5
| spl52_37
| spl52_1 ),
inference(avatar_split_clause,[],[f2089,f883,f2130,f907]) ).
fof(f2138,definition,
( spl52_38
<=> ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_lattice3(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_38])],[avatar_definition]) ).
fof(f2139,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v3_lattice3(X0) )
| ~ spl52_38 ),
inference(avatar_component_clause,[],[f2138]) ).
fof(f2140,plain,
( spl52_5
| spl52_38
| spl52_1
| ~ spl52_3 ),
inference(avatar_split_clause,[],[f2115,f891,f883,f2138,f907]) ).
fof(f2146,definition,
( spl52_39
<=> ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_39])],[avatar_definition]) ).
fof(f2147,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| v1_orders_2(X0) )
| ~ spl52_39 ),
inference(avatar_component_clause,[],[f2146]) ).
fof(f2148,plain,
( spl52_5
| spl52_39
| spl52_1
| ~ spl52_3 ),
inference(avatar_split_clause,[],[f2116,f891,f883,f2146,f907]) ).
fof(f2154,definition,
( spl52_40
<=> ! [X0] :
( ~ m1_subset_1(X0,sF51)
| r2_hidden(u1_struct_0(X0),sK0) ) ),
introduced(definition,[new_symbols(definition,[spl52_40])],[avatar_definition]) ).
fof(f2155,plain,
( ! [X0] :
( r2_hidden(u1_struct_0(X0),sK0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_40 ),
inference(avatar_component_clause,[],[f2154]) ).
fof(f2156,plain,
( spl52_5
| spl52_40
| spl52_1
| ~ spl52_3 ),
inference(avatar_split_clause,[],[f2114,f891,f883,f2154,f907]) ).
fof(f2233,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ l2_altcat_1(sF48)
| ~ v2_yellow21(sF48)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v6_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) ),
inference(superposition,[],[f770,f751]) ).
fof(f2247,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ v2_yellow21(sF48)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v6_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2233,f887]) ).
fof(f2249,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ v12_altcat_1(sF48)
| ~ v11_altcat_1(sF48)
| ~ v6_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2247,f864]) ).
fof(f2250,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ v11_altcat_1(sF48)
| ~ v6_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2249,f876]) ).
fof(f2251,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ v6_altcat_1(sF48)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2250,f862]) ).
fof(f2252,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ v2_altcat_1(sF48)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2251,f870]) ).
fof(f2253,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| v3_struct_0(sF48)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2252,f874]) ).
fof(f2254,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF48))
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_subsumption_resolution,[],[f2253,f857]) ).
fof(f2255,plain,
( ! [X0,X1] :
( m1_subset_1(X0,sF49)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_2 ),
inference(forward_demodulation,[],[f2254,f753]) ).
fof(f2257,definition,
( spl52_45
<=> ! [X0] :
( m1_subset_1(X0,sF49)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_45])],[avatar_definition]) ).
fof(f2258,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| m1_subset_1(X0,sF49)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) )
| ~ spl52_45 ),
inference(avatar_component_clause,[],[f2257]) ).
fof(f2259,plain,
( spl52_5
| spl52_45
| ~ spl52_2 ),
inference(avatar_split_clause,[],[f2255,f886,f2257,f907]) ).
fof(f2260,plain,
( ! [X0] :
( ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| m1_subset_1(X0,sF49)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_40
| ~ spl52_45 ),
inference(resolution,[],[f2258,f2155]) ).
fof(f2266,plain,
( ! [X0] :
( ~ v3_lattice3(X0)
| m1_subset_1(X0,sF49)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2260,f2147]) ).
fof(f2268,plain,
( ! [X0] :
( m1_subset_1(X0,sF49)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2266,f2139]) ).
fof(f2269,plain,
( ! [X0] :
( m1_subset_1(X0,sF49)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2268,f1447]) ).
fof(f2270,plain,
( ! [X0] :
( m1_subset_1(X0,sF49)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2269,f1500]) ).
fof(f2271,plain,
( ! [X0] :
( m1_subset_1(X0,sF49)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2270,f1544]) ).
fof(f2272,plain,
( ! [X0] :
( m1_subset_1(X0,sF49)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2271,f1565]) ).
fof(f2273,plain,
( ! [X0] :
( m1_subset_1(X0,sF49)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF51) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2272,f1518]) ).
fof(f2274,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF51)
| m1_subset_1(X0,sF49) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2273,f1419]) ).
fof(f2276,plain,
( ! [X0] :
( m1_subset_1(sK2(sF51,X0),sF49)
| r1_tarski(sF51,X0) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(resolution,[],[f2274,f1403]) ).
fof(f2294,plain,
( ! [X0] :
( r1_tarski(sF51,X0)
| r2_hidden(sK2(sF51,X0),sF49)
| v1_xboole_0(sF49) )
| ~ spl52_3
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(resolution,[],[f2276,f728]) ).
fof(f2295,plain,
( ! [X0] :
( r2_hidden(sK2(sF51,X0),sF49)
| r1_tarski(sF51,X0) )
| ~ spl52_3
| spl52_9
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2294,f960]) ).
fof(f2296,plain,
( r1_tarski(sF51,sF49)
| r1_tarski(sF51,sF49)
| ~ spl52_3
| spl52_9
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(resolution,[],[f2295,f407]) ).
fof(f2301,plain,
( r1_tarski(sF51,sF49)
| ~ spl52_3
| spl52_9
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(duplicate_literal_removal,[],[f2296]) ).
fof(f2304,plain,
( ~ r1_tarski(sF49,sF51)
| sF49 = sF51
| ~ spl52_3
| spl52_9
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(resolution,[],[f2301,f401]) ).
fof(f2305,plain,
( ~ r1_tarski(sF49,sF51)
| ~ spl52_3
| spl52_9
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45 ),
inference(forward_subsumption_resolution,[],[f2304,f758]) ).
fof(f2378,plain,
! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ l2_altcat_1(sF50)
| ~ v2_yellow21(sF50)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v6_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) ),
inference(superposition,[],[f762,f755]) ).
fof(f2395,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ v2_yellow21(sF50)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v6_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2378,f892]) ).
fof(f2397,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ v12_altcat_1(sF50)
| ~ v11_altcat_1(sF50)
| ~ v6_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2395,f868]) ).
fof(f2398,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ v11_altcat_1(sF50)
| ~ v6_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2397,f880]) ).
fof(f2399,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ v6_altcat_1(sF50)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2398,f866]) ).
fof(f2400,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ v2_altcat_1(sF50)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2399,f872]) ).
fof(f2401,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| v3_struct_0(sF50)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2400,f878]) ).
fof(f2402,plain,
( ! [X0,X1] :
( m1_subset_1(X0,u1_struct_0(sF50))
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_subsumption_resolution,[],[f2401,f859]) ).
fof(f2403,plain,
( ! [X0,X1] :
( m1_subset_1(X0,sF51)
| v1_xboole_0(X1)
| ~ l1_orders_2(X0)
| ~ v2_lattice3(X0)
| ~ v1_lattice3(X0)
| ~ v4_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v2_orders_2(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v3_lattice3(X0)
| ~ v1_orders_2(X0)
| ~ m1_subset_1(X1,sK0) )
| ~ spl52_3 ),
inference(forward_demodulation,[],[f2402,f757]) ).
fof(f2405,definition,
( spl52_47
<=> ! [X0] :
( m1_subset_1(X0,sF51)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_47])],[avatar_definition]) ).
fof(f2406,plain,
( ! [X0] :
( ~ r2_hidden(u1_struct_0(X0),sK0)
| ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| m1_subset_1(X0,sF51)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0) )
| ~ spl52_47 ),
inference(avatar_component_clause,[],[f2405]) ).
fof(f2407,plain,
( spl52_5
| spl52_47
| ~ spl52_3 ),
inference(avatar_split_clause,[],[f2403,f891,f2405,f907]) ).
fof(f2409,plain,
( ! [X0] :
( ~ v1_orders_2(X0)
| ~ v3_lattice3(X0)
| m1_subset_1(X0,sF51)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_6
| ~ spl52_47 ),
inference(resolution,[],[f2406,f911]) ).
fof(f2414,plain,
( ! [X0] :
( ~ v3_lattice3(X0)
| m1_subset_1(X0,sF51)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_6
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2409,f2131]) ).
fof(f2416,plain,
( ! [X0] :
( m1_subset_1(X0,sF51)
| ~ v2_orders_2(X0)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2414,f2123]) ).
fof(f2417,plain,
( ! [X0] :
( m1_subset_1(X0,sF51)
| ~ v3_orders_2(X0)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2416,f1448]) ).
fof(f2418,plain,
( ! [X0] :
( m1_subset_1(X0,sF51)
| ~ v4_orders_2(X0)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2417,f1501]) ).
fof(f2419,plain,
( ! [X0] :
( m1_subset_1(X0,sF51)
| ~ v1_lattice3(X0)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2418,f1545]) ).
fof(f2420,plain,
( ! [X0] :
( m1_subset_1(X0,sF51)
| ~ v2_lattice3(X0)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2419,f1566]) ).
fof(f2421,plain,
( ! [X0] :
( m1_subset_1(X0,sF51)
| ~ l1_orders_2(X0)
| ~ m1_subset_1(X0,sF49) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2420,f1519]) ).
fof(f2422,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF49)
| m1_subset_1(X0,sF51) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2421,f1420]) ).
fof(f2425,plain,
( ! [X0] :
( m1_subset_1(sK2(sF49,X0),sF51)
| r1_tarski(sF49,X0) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(resolution,[],[f2422,f1403]) ).
fof(f2445,plain,
( ! [X0] :
( r1_tarski(sF49,X0)
| r2_hidden(sK2(sF49,X0),sF51)
| v1_xboole_0(sF51) )
| ~ spl52_2
| ~ spl52_6
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(resolution,[],[f2425,f728]) ).
fof(f2446,plain,
( ! [X0] :
( r2_hidden(sK2(sF49,X0),sF51)
| r1_tarski(sF49,X0) )
| ~ spl52_2
| ~ spl52_6
| spl52_11
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2445,f967]) ).
fof(f2448,plain,
( r1_tarski(sF49,sF51)
| r1_tarski(sF49,sF51)
| ~ spl52_2
| ~ spl52_6
| spl52_11
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(resolution,[],[f2446,f407]) ).
fof(f2453,plain,
( r1_tarski(sF49,sF51)
| ~ spl52_2
| ~ spl52_6
| spl52_11
| ~ spl52_36
| ~ spl52_37
| ~ spl52_47 ),
inference(duplicate_literal_removal,[],[f2448]) ).
fof(f2455,plain,
( $false
| ~ spl52_2
| ~ spl52_3
| ~ spl52_6
| spl52_9
| spl52_11
| ~ spl52_36
| ~ spl52_37
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45
| ~ spl52_47 ),
inference(forward_subsumption_resolution,[],[f2453,f2305]) ).
fof(f2456,plain,
( ~ spl52_2
| ~ spl52_3
| ~ spl52_6
| spl52_9
| spl52_11
| ~ spl52_36
| ~ spl52_37
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45
| ~ spl52_47 ),
inference(avatar_contradiction_clause,[],[f2455]) ).
cnf(s416,plain,
( spl52_1
| spl52_2 ),
inference(sat_conversion,[],[f888]) ).
cnf(s419,plain,
( spl52_1
| spl52_3 ),
inference(sat_conversion,[],[f893]) ).
cnf(s422,plain,
~ spl52_1,
inference(sat_conversion,[],[f899]) ).
cnf(s426,plain,
( spl52_1
| spl52_5
| spl52_6 ),
inference(sat_conversion,[],[f912]) ).
cnf(s445,plain,
( ~ spl52_8
| ~ spl52_9 ),
inference(sat_conversion,[],[f961]) ).
cnf(s447,plain,
( ~ spl52_10
| ~ spl52_11 ),
inference(sat_conversion,[],[f968]) ).
cnf(s462,plain,
( ~ spl52_3
| spl52_10 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s463,plain,
( ~ spl52_2
| spl52_8 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s919,plain,
~ spl52_5,
inference(sat_conversion,[],[f2076]) ).
cnf(s931,plain,
( spl52_1
| spl52_5
| spl52_36 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s935,plain,
( spl52_1
| spl52_5
| spl52_37 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s939,plain,
( spl52_1
| ~ spl52_3
| spl52_5
| spl52_38 ),
inference(sat_conversion,[],[f2140]) ).
cnf(s943,plain,
( spl52_1
| ~ spl52_3
| spl52_5
| spl52_39 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s947,plain,
( spl52_1
| ~ spl52_3
| spl52_5
| spl52_40 ),
inference(sat_conversion,[],[f2156]) ).
cnf(s982,plain,
( ~ spl52_2
| spl52_5
| spl52_45 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s1015,plain,
( ~ spl52_3
| spl52_5
| spl52_47 ),
inference(sat_conversion,[],[f2407]) ).
cnf(s1023,plain,
( ~ spl52_2
| ~ spl52_3
| ~ spl52_6
| spl52_9
| spl52_11
| ~ spl52_36
| ~ spl52_37
| ~ spl52_38
| ~ spl52_39
| ~ spl52_40
| ~ spl52_45
| ~ spl52_47 ),
inference(sat_conversion,[],[f2456]) ).
cnf(s1026,plain,
( spl52_1
| spl52_6 ),
inference(rat,[],[s426,s919]) ).
cnf(s1029,plain,
spl52_37,
inference(rat,[],[s935,s919,s422]) ).
cnf(s1030,plain,
spl52_36,
inference(rat,[],[s931,s919,s422]) ).
cnf(s1033,plain,
spl52_6,
inference(rat,[],[s1026,s422]) ).
cnf(s1035,plain,
spl52_3,
inference(rat,[],[s419,s422]) ).
cnf(s1036,plain,
spl52_47,
inference(rat,[],[s1015,s919,s1035]) ).
cnf(s1037,plain,
spl52_40,
inference(rat,[],[s947,s422,s919,s1035]) ).
cnf(s1038,plain,
spl52_39,
inference(rat,[],[s943,s422,s919,s1035]) ).
cnf(s1039,plain,
spl52_38,
inference(rat,[],[s939,s422,s919,s1035]) ).
cnf(s1040,plain,
spl52_10,
inference(rat,[],[s462,s1035]) ).
cnf(s1041,plain,
~ spl52_11,
inference(rat,[],[s447,s1040]) ).
cnf(s1042,plain,
spl52_2,
inference(rat,[],[s416,s422]) ).
cnf(s1043,plain,
spl52_45,
inference(rat,[],[s982,s919,s1042]) ).
cnf(s1044,plain,
spl52_8,
inference(rat,[],[s463,s1042]) ).
cnf(s1045,plain,
spl52_9,
inference(rat,[],[s1023,s1036,s1042,s1037,s1038,s1039,s1029,s1030,s1041,s1035,s1033,s1043]) ).
cnf(s1046,plain,
$false,
inference(rat,[],[s445,s1045,s1044]) ).
fof(f2457,plain,
$false,
inference(avatar_sat_refutation,[],[s1046]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT360+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n001.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 15:06:16 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.93/2.42 % (3667759)Detected formulas, will run a generic FOF schedule.
% 10.93/2.42 % (3667768)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2487505692:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.93/2.42 % (3667768)Instruction limit reached!
% 10.93/2.42 % (3667768)------------------------------
% 10.93/2.42 % (3667768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.42 % (3667768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.42 % (3667768)CaDiCaL version: 2.1.3
% 10.93/2.42 % (3667768)Termination reason: Instruction limit
% 10.93/2.42 % (3667768)Termination phase: Saturation
% 10.93/2.42 % (3667768)Time elapsed: 0.037 s
% 10.93/2.42 % (3667768)Peak memory usage: 89 MB
% 10.93/2.42 % (3667768)Instructions burned: 122 (million)
% 10.93/2.42 % (3667769)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4127344650:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.93/2.42 % (3667764)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=3483635072:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.93/2.42 % (3667766)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=2280942594:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.93/2.42 % (3667770)dis-21_1_sil=8000:lcm=predicate:random_seed=3736870681: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)
% 10.93/2.42 % (3667767)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4140999717:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.93/2.42 % (3667765)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=1284735749:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.93/2.42 % (3667767)Refutation not found, incomplete strategy
% 10.93/2.42 % (3667767)------------------------------
% 10.93/2.42 % (3667767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.42 % (3667767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.42 % (3667767)CaDiCaL version: 2.1.3
% 10.93/2.42 % (3667767)Termination reason: Refutation not found, incomplete strategy
% 10.93/2.42 % (3667767)Time elapsed: 0.002 s
% 10.93/2.42 % (3667767)Peak memory usage: 88 MB
% 10.93/2.42 % (3667767)Instructions burned: 1 (million)
% 10.93/2.42 % (3667770)Instruction limit reached!
% 10.93/2.42 % (3667770)------------------------------
% 10.93/2.42 % (3667770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.42 % (3667770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.42 % (3667770)CaDiCaL version: 2.1.3
% 10.93/2.42 % (3667770)Termination reason: Instruction limit
% 10.93/2.42 % (3667770)Termination phase: Saturation
% 10.93/2.42 % (3667770)Time elapsed: 0.078 s
% 10.93/2.42 % (3667770)Peak memory usage: 92 MB
% 10.93/2.42 % (3667770)Instructions burned: 129 (million)
% 10.93/2.42 % (3667778)lrs+10_1_sil=8000:sp=occurrence:random_seed=3103098513:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 10.93/2.42 % (3667769)Instruction limit reached!
% 10.93/2.42 % (3667769)------------------------------
% 10.93/2.42 % (3667769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.42 % (3667769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.42 % (3667769)CaDiCaL version: 2.1.3
% 10.93/2.42 % (3667769)Termination reason: Instruction limit
% 10.93/2.42 % (3667769)Termination phase: Saturation
% 10.93/2.42 % (3667769)Time elapsed: 0.097 s
% 10.93/2.42 % (3667769)Peak memory usage: 90 MB
% 10.93/2.42 % (3667769)Instructions burned: 140 (million)
% 10.93/2.42 % (3667778)Instruction limit reached!
% 10.93/2.42 % (3667778)------------------------------
% 10.93/2.42 % (3667778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.93/2.42 % (3667778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.93/2.42 % (3667778)CaDiCaL version: 2.1.3
% 10.93/2.42 % (3667778)Termination reason: Instruction limit
% 10.93/2.42 % (3667778)Termination phase: Saturation
% 10.93/2.42 % (3667778)Time elapsed: 0.088 s
% 10.93/2.42 % (3667778)Peak memory usage: 92 MB
% 10.93/2.42 % (3667778)Instructions burned: 288 (million)
% 16.66/3.30 % (3667779)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3526718390:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 16.66/3.30 % (3667781)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2742360121:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 16.66/3.30 % (3667779)Refutation not found, incomplete strategy
% 16.66/3.30 % (3667779)------------------------------
% 16.66/3.30 % (3667779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.30 % (3667779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.30 % (3667779)CaDiCaL version: 2.1.3
% 16.66/3.30 % (3667779)Termination reason: Refutation not found, incomplete strategy
% 16.66/3.30 % (3667779)Time elapsed: 0.013 s
% 16.66/3.30 % (3667779)Peak memory usage: 89 MB
% 16.66/3.30 % (3667779)Instructions burned: 20 (million)
% 16.66/3.30 % (3667767)------------------------------
% 16.66/3.30 % (3667767)------------------------------
% 16.66/3.30 % (3667782)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=2709143964:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 16.66/3.30 % (3667782)Instruction limit reached!
% 16.66/3.30 % (3667782)------------------------------
% 16.66/3.30 % (3667782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.30 % (3667782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.30 % (3667782)CaDiCaL version: 2.1.3
% 16.66/3.30 % (3667782)Termination reason: Instruction limit
% 16.66/3.30 % (3667782)Termination phase: Saturation
% 16.66/3.30 % (3667782)Time elapsed: 0.069 s
% 16.66/3.30 % (3667782)Peak memory usage: 90 MB
% 16.66/3.30 % (3667782)Instructions burned: 251 (million)
% 16.66/3.30 % (3667785)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2715148125:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 16.66/3.30 % (3667785)Refutation not found, incomplete strategy
% 16.66/3.30 % (3667785)------------------------------
% 16.66/3.30 % (3667785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.30 % (3667785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.30 % (3667785)CaDiCaL version: 2.1.3
% 16.66/3.30 % (3667785)Termination reason: Refutation not found, incomplete strategy
% 16.66/3.30 % (3667785)Time elapsed: 0.011 s
% 16.66/3.30 % (3667785)Peak memory usage: 89 MB
% 16.66/3.30 % (3667785)Instructions burned: 17 (million)
% 16.66/3.30 % (3667787)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=21687352:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 16.66/3.30 % (3667781)Instruction limit reached!
% 16.66/3.30 % (3667781)------------------------------
% 16.66/3.30 % (3667781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.30 % (3667781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.30 % (3667781)CaDiCaL version: 2.1.3
% 16.66/3.30 % (3667781)Termination reason: Instruction limit
% 16.66/3.30 % (3667781)Termination phase: Saturation
% 16.66/3.30 % (3667781)Time elapsed: 0.205 s
% 16.66/3.30 % (3667781)Peak memory usage: 92 MB
% 16.66/3.30 % (3667781)Instructions burned: 325 (million)
% 16.66/3.30 % (3667779)------------------------------
% 16.66/3.30 % (3667779)------------------------------
% 16.66/3.30 % (3667790)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1654496521:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 16.66/3.30 % (3667790)Instruction limit reached!
% 16.66/3.30 % (3667790)------------------------------
% 16.66/3.30 % (3667790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.66/3.30 % (3667790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.66/3.30 % (3667790)CaDiCaL version: 2.1.3
% 16.66/3.30 % (3667790)Termination reason: Instruction limit
% 16.66/3.30 % (3667790)Termination phase: Saturation
% 16.66/3.30 % (3667790)Time elapsed: 0.068 s
% 16.66/3.30 % (3667790)Peak memory usage: 92 MB
% 16.66/3.30 % (3667790)Instructions burned: 114 (million)
% 16.66/3.30 % (3667791)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1974590024:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 16.66/3.30 % (3667785)------------------------------
% 16.66/3.30 % (3667785)------------------------------
% 16.66/3.30 % (3667791)Instruction limit reached!
% 16.66/3.30 % (3667791)------------------------------
% 16.66/3.30 % (3667791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667791)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667791)Termination reason: Instruction limit
% 25.37/4.45 % (3667791)Termination phase: Saturation
% 25.37/4.45 % (3667791)Time elapsed: 0.065 s
% 25.37/4.45 % (3667791)Peak memory usage: 89 MB
% 25.37/4.45 % (3667791)Instructions burned: 127 (million)
% 25.37/4.45 % (3667794)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=474413498:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 25.37/4.45 % (3667795)lrs+10_1_sil=8000:sp=occurrence:random_seed=1686772428:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 25.37/4.45 % (3667794)Instruction limit reached!
% 25.37/4.45 % (3667794)------------------------------
% 25.37/4.45 % (3667794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667794)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667794)Termination reason: Instruction limit
% 25.37/4.45 % (3667794)Termination phase: Saturation
% 25.37/4.45 % (3667794)Time elapsed: 0.063 s
% 25.37/4.45 % (3667794)Peak memory usage: 89 MB
% 25.37/4.45 % (3667794)Instructions burned: 116 (million)
% 25.37/4.45 % (3667796)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2099612908:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 25.37/4.45 % (3667796)Refutation not found, incomplete strategy
% 25.37/4.45 % (3667796)------------------------------
% 25.37/4.45 % (3667796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667796)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667796)Termination reason: Refutation not found, incomplete strategy
% 25.37/4.45 % (3667796)Time elapsed: 0.012 s
% 25.37/4.45 % (3667796)Peak memory usage: 89 MB
% 25.37/4.45 % (3667796)Instructions burned: 20 (million)
% 25.37/4.45 % (3667799)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3735471004:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 25.37/4.45 % (3667796)------------------------------
% 25.37/4.45 % (3667796)------------------------------
% 25.37/4.45 % (3667802)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2351041663:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 25.37/4.45 % (3667795)Instruction limit reached!
% 25.37/4.45 % (3667795)------------------------------
% 25.37/4.45 % (3667795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667795)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667795)Termination reason: Instruction limit
% 25.37/4.45 % (3667795)Termination phase: Saturation
% 25.37/4.45 % (3667795)Time elapsed: 0.485 s
% 25.37/4.45 % (3667795)Peak memory usage: 99 MB
% 25.37/4.45 % (3667795)Instructions burned: 909 (million)
% 25.37/4.45 % (3667787)Instruction limit reached!
% 25.37/4.45 % (3667787)------------------------------
% 25.37/4.45 % (3667787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667787)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667787)Termination reason: Instruction limit
% 25.37/4.45 % (3667787)Termination phase: Saturation
% 25.37/4.45 % (3667787)Time elapsed: 0.847 s
% 25.37/4.45 % (3667787)Peak memory usage: 142 MB
% 25.37/4.45 % (3667787)Instructions burned: 2351 (million)
% 25.37/4.45 % (3667802)Instruction limit reached!
% 25.37/4.45 % (3667802)------------------------------
% 25.37/4.45 % (3667802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667802)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667802)Termination reason: Instruction limit
% 25.37/4.45 % (3667802)Termination phase: Saturation
% 25.37/4.45 % (3667802)Time elapsed: 0.070 s
% 25.37/4.45 % (3667802)Peak memory usage: 90 MB
% 25.37/4.45 % (3667802)Instructions burned: 135 (million)
% 25.37/4.45 % (3667805)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=919354789:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 25.37/4.45 % (3667804)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1162397274:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 25.37/4.45 % (3667806)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=619227381:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/125Mi)
% 25.37/4.45 % (3667806)Instruction limit reached!
% 25.37/4.45 % (3667806)------------------------------
% 25.37/4.45 % (3667806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667806)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667806)Termination reason: Instruction limit
% 25.37/4.45 % (3667806)Termination phase: Saturation
% 25.37/4.45 % (3667806)Time elapsed: 0.078 s
% 25.37/4.45 % (3667806)Peak memory usage: 91 MB
% 25.37/4.45 % (3667806)Instructions burned: 127 (million)
% 25.37/4.45 % (3667810)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2213651146:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 25.37/4.45 % (3667804)Instruction limit reached!
% 25.37/4.45 % (3667804)------------------------------
% 25.37/4.45 % (3667804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667804)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667804)Termination reason: Instruction limit
% 25.37/4.45 % (3667804)Termination phase: Saturation
% 25.37/4.45 % (3667804)Time elapsed: 0.290 s
% 25.37/4.45 % (3667804)Peak memory usage: 92 MB
% 25.37/4.45 % (3667804)Instructions burned: 593 (million)
% 25.37/4.45 % (3667810)Instruction limit reached!
% 25.37/4.45 % (3667810)------------------------------
% 25.37/4.45 % (3667810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667810)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667810)Termination reason: Instruction limit
% 25.37/4.45 % (3667810)Termination phase: Saturation
% 25.37/4.45 % (3667810)Time elapsed: 0.083 s
% 25.37/4.45 % (3667810)Peak memory usage: 91 MB
% 25.37/4.45 % (3667810)Instructions burned: 135 (million)
% 25.37/4.45 % (3667813)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2394514086:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2981 on theBenchmark for (2981ds/431Mi)
% 25.37/4.45 % (3667812)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=920248826:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 25.37/4.45 % (3667812)Refutation not found, incomplete strategy
% 25.37/4.45 % (3667812)------------------------------
% 25.37/4.45 % (3667812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667812)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667812)Termination reason: Refutation not found, incomplete strategy
% 25.37/4.45 % (3667812)Time elapsed: 0.018 s
% 25.37/4.45 % (3667812)Peak memory usage: 89 MB
% 25.37/4.45 % (3667812)Instructions burned: 33 (million)
% 25.37/4.45 % (3667813)Instruction limit reached!
% 25.37/4.45 % (3667813)------------------------------
% 25.37/4.45 % (3667813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667813)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667813)Termination reason: Instruction limit
% 25.37/4.45 % (3667813)Termination phase: Saturation
% 25.37/4.45 % (3667813)Time elapsed: 0.233 s
% 25.37/4.45 % (3667813)Peak memory usage: 93 MB
% 25.37/4.45 % (3667813)Instructions burned: 433 (million)
% 25.37/4.45 % (3667812)------------------------------
% 25.37/4.45 % (3667812)------------------------------
% 25.37/4.45 % (3667816)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=4098876569:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 25.37/4.45 % (3667817)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=1535893680:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 25.37/4.45 % (3667817)Instruction limit reached!
% 25.37/4.45 % (3667817)------------------------------
% 25.37/4.45 % (3667817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.37/4.45 % (3667817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/4.45 % (3667817)CaDiCaL version: 2.1.3
% 25.37/4.45 % (3667817)Termination reason: Instruction limit
% 25.37/4.45 % (3667817)Termination phase: Saturation
% 25.37/4.45 % (3667817)Time elapsed: 0.085 s
% 25.37/4.45 % (3667817)Peak memory usage: 92 MB
% 25.37/4.45 % (3667817)Instructions burned: 152 (million)
% 25.37/4.45 % (3667820)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1006202733:i=14155:bd=all_2975 on theBenchmark for (2975ds/14155Mi)
% 25.37/4.45 % (3667816)First to succeed.
% 25.37/4.45 % (3667816)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3667759"
% 25.37/4.45 % (3667816)Refutation found. Thanks to Tanya!
% 25.37/4.45 % SZS status Theorem for theBenchmark
% 25.37/4.45 % SZS output start Proof for theBenchmark
% See solution above
% 25.90/4.65 % (3667816)------------------------------
% 25.90/4.65 % (3667816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.90/4.65 % (3667816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.90/4.65 % (3667816)CaDiCaL version: 2.1.3
% 25.90/4.65 % (3667816)Termination reason: Refutation
% 25.90/4.65 % (3667816)Time elapsed: 0.974 s
% 25.90/4.65 % (3667816)Peak memory usage: 137 MB
% 25.90/4.65 % (3667816)Instructions burned: 1476 (million)
% 25.90/4.65 % (3667816)------------------------------
% 25.90/4.65 % (3667816)------------------------------
% 25.90/4.65 % (3667759)Success in time 3.578 s
% 25.90/4.65 % Vampire exiting
%------------------------------------------------------------------------------