%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SCT030-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:07:36 PM UTC 2026
% Result : Unsatisfiable 27.46s 4.59s
% Output : CNFRefutation 27.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 68
% Syntax : Number of clauses : 338 ( 117 unt; 62 nHn; 189 RR)
% Number of literals : 641 ( 196 equ; 286 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 7 con; 0-5 aty)
% Number of variables : 668 ( 153 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_order__less__le_1,axiom,
( ~ c_HOL_Oord__class_Oless(X2,X2,X1)
| ~ class_Orderings_Oorder(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
cnf(cls_less__supI2_0,axiom,
( ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_HOL_Oord__class_Oless(X2,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X3,X1),X4),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__supI2_0) ).
cnf(cls_sup__absorb1_0,axiom,
( ~ c_lessequals(X3,X2,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__absorb1_0) ).
cnf(cls_top__greatest_0,axiom,
( ~ class_Orderings_Otop(X1)
| c_lessequals(X2,c_Orderings_Otop__class_Otop(X1),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_top__greatest_0) ).
cnf(clsarity_bool__Lattices_Oupper__semilattice,axiom,
class_Lattices_Oupper__semilattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Oupper__semilattice) ).
cnf(cls_bot__least_0,axiom,
( ~ class_Orderings_Obot(X1)
| c_lessequals(c_Orderings_Obot__class_Obot(X1),X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot__least_0) ).
cnf(cls_xt1_I8_J_0,axiom,
( ~ c_lessequals(X4,X3,X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Orderings_Oorder(X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I8_J_0) ).
cnf(clsarity_bool__Orderings_Otop,axiom,
class_Orderings_Otop(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Orderings_Otop) ).
cnf(cls_xt1_I11_J_0,axiom,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| X3 = X2
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I11_J_0) ).
cnf(clsarity_bool__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Orderings_Oorder) ).
cnf(cls_less__infI1_0,axiom,
( ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Lattices_Olower__semilattice(X1)
| c_HOL_Oord__class_Oless(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3),X4,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__infI1_0) ).
cnf(cls_diff__eq_0,axiom,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ominus__class_Ominus(X2,X1),X3) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__eq_0) ).
cnf(cls_xt1_I7_J_0,axiom,
( ~ c_HOL_Oord__class_Oless(X4,X3,X1)
| ~ c_lessequals(X2,X4,X1)
| ~ class_Orderings_Oorder(X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I7_J_0) ).
cnf(clsarity_bool__Orderings_Obot,axiom,
class_Orderings_Obot(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Orderings_Obot) ).
cnf(cls_less__le__not__le_1,axiom,
( ~ c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
cnf(cls_less__supI1_0,axiom,
( ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_HOL_Oord__class_Oless(X2,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X3,X1),X4),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__supI1_0) ).
cnf(cls_le__funD_0,axiom,
( ~ c_lessequals(X2,X4,tc_fun(X5,X1))
| ~ class_HOL_Oord(X1)
| c_lessequals(hAPP(X2,X3),hAPP(X4,X3),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__funD_0) ).
cnf(clsarity_bool__Lattices_Olower__semilattice,axiom,
class_Lattices_Olower__semilattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Olower__semilattice) ).
cnf(clsarity_bool__Lattices_Oboolean__algebra,axiom,
class_Lattices_Oboolean__algebra(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Oboolean__algebra) ).
cnf(cls_Collect__mem__eq_0,axiom,
c_Collect(hAPP(c_COMBC(c_in(X1),X1,tc_fun(X1,tc_bool),tc_bool),X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__mem__eq_0) ).
cnf(cls_Collect__def_0,axiom,
c_Collect(X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__def_0) ).
cnf(cls_subset__UNIV_0,axiom,
c_lessequals(X1,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subset__UNIV_0) ).
cnf(clsarity_bool__HOL_Oord,axiom,
class_HOL_Oord(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__HOL_Oord) ).
cnf(cls_empty__subsetI_0,axiom,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__subsetI_0) ).
cnf(cls_vimage__Collect__eq_0,axiom,
hAPP(c_Set_Ovimage(X1,X2,X3),c_Collect(X4,X3)) = c_Collect(c_COMBB(X4,X1,X3,tc_bool,X2),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_vimage__Collect__eq_0) ).
cnf(cls_vimage__const_0,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X4))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_vimage__const_0) ).
cnf(cls_COMBC__def_0,axiom,
hAPP(hAPP(c_COMBC(X1,X2,X3,X4),X5),X6) = hAPP(hAPP(X1,X6),X5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_COMBC__def_0) ).
cnf(clsarity_bool__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Orderings_Opreorder) ).
cnf(cls_sup__inf__absorb_0,axiom,
( ~ class_Lattices_Olattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__inf__absorb_0) ).
cnf(cls_COMBB__def_0,axiom,
hAPP(c_COMBB(X1,X2,X3,X4,X5),X6) = hAPP(X1,hAPP(X2,X6)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_COMBB__def_0) ).
cnf(cls_vimage__const_1,axiom,
( hBOOL(hAPP(hAPP(c_in(X2),X1),X4))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_vimage__const_1) ).
cnf(clsarity_bool__Lattices_Olattice,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Olattice) ).
cnf(cls_insert__absorb_0,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X3))
| hAPP(c_Set_Oinsert(X1,X2),X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
cnf(cls_COMBK__def_0,axiom,
hAPP(c_COMBK(X1,X2,X3),X4) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_COMBK__def_0) ).
cnf(cls_Collect__neg__eq_0,axiom,
c_Collect(c_COMBB(c_Not,X1,tc_bool,tc_bool,X2),X2) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X2,tc_bool)),c_Collect(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Collect__neg__eq_0) ).
cnf(cls_compl__sup_0,axiom,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3)) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2),X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_compl__sup_0) ).
cnf(cls_le__iff__sup_0,axiom,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3) = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__iff__sup_0) ).
cnf(cls_empty__not__insert_0,axiom,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) != hAPP(c_Set_Oinsert(X2,X1),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
cnf(cls_CHAINED_0,axiom,
hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_P____),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
cnf(cls_vimage__code_0,axiom,
( ~ hBOOL(hAPP(hAPP(c_Set_Ovimage(X2,X4,X5),X1),X3))
| hBOOL(hAPP(X1,hAPP(X2,X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_vimage__code_0) ).
cnf(cls_ComplI_0,axiom,
( hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| hBOOL(hAPP(hAPP(c_in(X1),X2),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplI_0) ).
cnf(cls_compl__top__eq_0,axiom,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),c_Orderings_Otop__class_Otop(X1)) = c_Orderings_Obot__class_Obot(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_compl__top__eq_0) ).
cnf(cls_inf__top__left_0,axiom,
( ~ class_Lattices_Obounded__lattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(X1),X1),X2) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__top__left_0) ).
cnf(cls_set__insert_0,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(X3),X2),X1))
| X1 = hAPP(c_Set_Oinsert(X2,X3),c_ATP__Linkup_Osko__Set__Xset__insert__1__1(X1,X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_set__insert_0) ).
cnf(cls_rev__bexI_0,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X4),X2))
| ~ hBOOL(hAPP(X3,X4))
| hBOOL(hAPP(hAPP(c_in(X1),c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(X2,X3,X1)),X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rev__bexI_0) ).
cnf(cls_double__compl_0,axiom,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_double__compl_0) ).
cnf(cls_le__iff__inf_1,axiom,
( hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3) != X2
| ~ class_Lattices_Olower__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__iff__inf_1) ).
cnf(clsarity_bool__Lattices_Obounded__lattice,axiom,
class_Lattices_Obounded__lattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_bool__Lattices_Obounded__lattice) ).
cnf(cls_order__eq__iff_0,axiom,
( ~ class_Orderings_Oorder(X1)
| c_lessequals(X2,X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__eq__iff_0) ).
cnf(cls_less__le__not__le_2,axiom,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1)
| c_lessequals(X3,X2,X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_2) ).
cnf(cls_sup__bot__right_0,axiom,
( ~ class_Lattices_Obounded__lattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),c_Orderings_Obot__class_Obot(X1)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup__bot__right_0) ).
cnf(cls_le__supE_0,axiom,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X4),X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__supE_0) ).
cnf(cls_le__supE_1,axiom,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X4,X1),X2),X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__supE_1) ).
cnf(cls_Compl__empty__eq_0,axiom,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))) = c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Compl__empty__eq_0) ).
cnf(cls_top1I_0,axiom,
hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_top1I_0) ).
cnf(cls_bot1E_0,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
cnf(cls_CollectI_0,axiom,
( ~ hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(hAPP(c_in(X1),X2),c_Collect(X3,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CollectI_0) ).
cnf(cls_inf__commute_0,axiom,
( ~ class_Lattices_Olower__semilattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X3,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__commute_0) ).
cnf(cls_compl__bot__eq_0,axiom,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),c_Orderings_Obot__class_Obot(X1)) = c_Orderings_Otop__class_Otop(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_compl__bot__eq_0) ).
cnf(cls_conjecture_0,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_inf__compl__bot_0,axiom,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2)) = c_Orderings_Obot__class_Obot(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__compl__bot_0) ).
cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom,
hBOOL(hAPP(hAPP(c_fequal(X1),X2),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ATP__Linkup_Oequal__imp__fequal_0) ).
cnf(cls_singleton__conv2_0,axiom,
c_Collect(hAPP(c_fequal(X1),X2),X1) = hAPP(c_Set_Oinsert(X2,X1),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_singleton__conv2_0) ).
cnf(cls_inf__idem_0,axiom,
( ~ class_Lattices_Olower__semilattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X2) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inf__idem_0) ).
cnf(cls_order__antisym__conv_0,axiom,
( ~ c_lessequals(X3,X2,X1)
| ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| X2 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__antisym__conv_0) ).
cnf(cls_ComplD_0,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X2),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X3)))
| ~ hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
cnf(cls_vimage__code_1,axiom,
( ~ hBOOL(hAPP(X4,hAPP(X1,X5)))
| hBOOL(hAPP(hAPP(c_Set_Ovimage(X1,X2,X3),X4),X5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_vimage__code_1) ).
cnf(cls_double__complement_0,axiom,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_double__complement_0) ).
cnf(c_0_68,plain,
( ~ c_HOL_Oord__class_Oless(X2,X2,X1)
| ~ class_Orderings_Oorder(X1) ),
inference(fof_simplification,[status(thm)],[cls_order__less__le_1]) ).
cnf(c_0_69,plain,
( ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_HOL_Oord__class_Oless(X2,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X3,X1),X4),X1) ),
inference(fof_simplification,[status(thm)],[cls_less__supI2_0]) ).
cnf(c_0_70,plain,
( ~ c_lessequals(X3,X2,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3) = X2 ),
inference(fof_simplification,[status(thm)],[cls_sup__absorb1_0]) ).
cnf(c_0_71,plain,
( ~ class_Orderings_Otop(X1)
| c_lessequals(X2,c_Orderings_Otop__class_Otop(X1),X1) ),
inference(fof_simplification,[status(thm)],[cls_top__greatest_0]) ).
cnf(c_0_72,plain,
( ~ c_HOL_Oord__class_Oless(X2,X2,X1)
| ~ class_Orderings_Oorder(X1) ),
c_0_68 ).
cnf(c_0_73,plain,
( ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_HOL_Oord__class_Oless(X2,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X3,X1),X4),X1) ),
c_0_69 ).
cnf(c_0_74,plain,
( ~ c_lessequals(X3,X2,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3) = X2 ),
c_0_70 ).
cnf(c_0_75,axiom,
class_Lattices_Oupper__semilattice(tc_bool),
clsarity_bool__Lattices_Oupper__semilattice ).
cnf(c_0_76,plain,
( ~ class_Orderings_Obot(X1)
| c_lessequals(c_Orderings_Obot__class_Obot(X1),X2,X1) ),
inference(fof_simplification,[status(thm)],[cls_bot__least_0]) ).
cnf(c_0_77,plain,
( ~ c_lessequals(X4,X3,X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Orderings_Oorder(X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_xt1_I8_J_0]) ).
cnf(c_0_78,plain,
( ~ class_Orderings_Otop(X1)
| c_lessequals(X2,c_Orderings_Otop__class_Otop(X1),X1) ),
c_0_71 ).
cnf(c_0_79,axiom,
class_Orderings_Otop(tc_bool),
clsarity_bool__Orderings_Otop ).
cnf(c_0_80,plain,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| X3 = X2
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_xt1_I11_J_0]) ).
cnf(c_0_81,plain,
( ~ class_Orderings_Oorder(X2)
| ~ class_Lattices_Oupper__semilattice(X2)
| ~ c_HOL_Oord__class_Oless(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X2),X3),X3,X2) ),
inference(spm,[status(thm)],[c_0_72,c_0_73]) ).
cnf(c_0_82,plain,
( ~ c_lessequals(X2,X1,tc_bool)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2) = X1 ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_83,axiom,
class_Orderings_Oorder(tc_bool),
clsarity_bool__Orderings_Oorder ).
cnf(c_0_84,plain,
( ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Lattices_Olower__semilattice(X1)
| c_HOL_Oord__class_Oless(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3),X4,X1) ),
inference(fof_simplification,[status(thm)],[cls_less__infI1_0]) ).
cnf(c_0_85,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ominus__class_Ominus(X2,X1),X3) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X3)) ),
inference(fof_simplification,[status(thm)],[cls_diff__eq_0]) ).
cnf(c_0_86,plain,
( ~ c_HOL_Oord__class_Oless(X4,X3,X1)
| ~ c_lessequals(X2,X4,X1)
| ~ class_Orderings_Oorder(X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_xt1_I7_J_0]) ).
cnf(c_0_87,plain,
( ~ class_Orderings_Obot(X1)
| c_lessequals(c_Orderings_Obot__class_Obot(X1),X2,X1) ),
c_0_76 ).
cnf(c_0_88,axiom,
class_Orderings_Obot(tc_bool),
clsarity_bool__Orderings_Obot ).
cnf(c_0_89,plain,
( ~ c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1) ),
inference(fof_simplification,[status(thm)],[cls_less__le__not__le_1]) ).
cnf(c_0_90,plain,
( ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_HOL_Oord__class_Oless(X2,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X3,X1),X4),X1) ),
inference(fof_simplification,[status(thm)],[cls_less__supI1_0]) ).
cnf(c_0_91,plain,
( ~ c_lessequals(X2,X4,tc_fun(X5,X1))
| ~ class_HOL_Oord(X1)
| c_lessequals(hAPP(X2,X3),hAPP(X4,X3),X1) ),
inference(fof_simplification,[status(thm)],[cls_le__funD_0]) ).
cnf(c_0_92,plain,
( ~ c_lessequals(X4,X3,X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Orderings_Oorder(X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
c_0_77 ).
cnf(c_0_93,plain,
c_lessequals(X1,c_Orderings_Otop__class_Otop(tc_bool),tc_bool),
inference(spm,[status(thm)],[c_0_78,c_0_79]) ).
cnf(c_0_94,plain,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| X3 = X2
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
c_0_80 ).
cnf(c_0_95,plain,
( ~ c_lessequals(X2,X1,tc_bool)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_82]),c_0_75]),c_0_83])]) ).
cnf(c_0_96,plain,
( ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ class_Lattices_Olower__semilattice(X1)
| c_HOL_Oord__class_Oless(hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3),X4,X1) ),
c_0_84 ).
cnf(c_0_97,axiom,
class_Lattices_Olower__semilattice(tc_bool),
clsarity_bool__Lattices_Olower__semilattice ).
cnf(c_0_98,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ominus__class_Ominus(X2,X1),X3) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X3)) ),
c_0_85 ).
cnf(c_0_99,axiom,
class_Lattices_Oboolean__algebra(tc_bool),
clsarity_bool__Lattices_Oboolean__algebra ).
cnf(c_0_100,plain,
( ~ c_HOL_Oord__class_Oless(X4,X3,X1)
| ~ c_lessequals(X2,X4,X1)
| ~ class_Orderings_Oorder(X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
c_0_86 ).
cnf(c_0_101,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_bool),X1,tc_bool),
inference(spm,[status(thm)],[c_0_87,c_0_88]) ).
cnf(c_0_102,axiom,
c_Collect(hAPP(c_COMBC(c_in(X1),X1,tc_fun(X1,tc_bool),tc_bool),X2),X1) = X2,
cls_Collect__mem__eq_0 ).
cnf(c_0_103,axiom,
c_Collect(X1,X2) = X1,
cls_Collect__def_0 ).
cnf(c_0_104,plain,
( ~ c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1) ),
c_0_89 ).
cnf(c_0_105,plain,
( ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_HOL_Oord__class_Oless(X2,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X3,X1),X4),X1) ),
c_0_90 ).
cnf(c_0_106,plain,
( ~ c_lessequals(X2,X4,tc_fun(X5,X1))
| ~ class_HOL_Oord(X1)
| c_lessequals(hAPP(X2,X3),hAPP(X4,X3),X1) ),
c_0_91 ).
cnf(c_0_107,axiom,
c_lessequals(X1,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_bool)),tc_fun(X2,tc_bool)),
cls_subset__UNIV_0 ).
cnf(c_0_108,axiom,
class_HOL_Oord(tc_bool),
clsarity_bool__HOL_Oord ).
cnf(c_0_109,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,tc_bool)
| c_HOL_Oord__class_Oless(X1,c_Orderings_Otop__class_Otop(tc_bool),tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_93]),c_0_83])]) ).
cnf(c_0_110,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| c_HOL_Oord__class_Oless(X1,X2,tc_bool)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_94,c_0_83]) ).
cnf(c_0_111,plain,
( ~ c_lessequals(X2,hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),X3),tc_bool)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95,c_0_96]),c_0_97])]) ).
cnf(c_0_112,plain,
hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X2)) = hAPP(c_HOL_Ominus__class_Ominus(X1,tc_bool),X2),
inference(spm,[status(thm)],[c_0_98,c_0_99]) ).
cnf(c_0_113,axiom,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)),
cls_empty__subsetI_0 ).
cnf(c_0_114,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_bool)
| c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),X1,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100,c_0_101]),c_0_83])]) ).
cnf(c_0_115,axiom,
hAPP(c_Set_Ovimage(X1,X2,X3),c_Collect(X4,X3)) = c_Collect(c_COMBB(X4,X1,X3,tc_bool,X2),X2),
cls_vimage__Collect__eq_0 ).
cnf(c_0_116,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X4))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)) ),
inference(fof_simplification,[status(thm)],[cls_vimage__const_0]) ).
cnf(c_0_117,axiom,
hAPP(hAPP(c_COMBC(X1,X2,X3,X4),X5),X6) = hAPP(hAPP(X1,X6),X5),
cls_COMBC__def_0 ).
cnf(c_0_118,plain,
hAPP(c_COMBC(c_in(X1),X1,tc_fun(X1,tc_bool),tc_bool),X2) = X2,
inference(rw,[status(thm)],[c_0_102,c_0_103]) ).
cnf(c_0_119,plain,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X3),X4),X1,X3)
| ~ class_Lattices_Oupper__semilattice(X3)
| ~ class_Orderings_Opreorder(X3)
| ~ c_HOL_Oord__class_Oless(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
cnf(c_0_120,plain,
c_lessequals(hAPP(X1,X2),hAPP(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)),X2),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_107]),c_0_108])]) ).
cnf(c_0_121,axiom,
class_Orderings_Opreorder(tc_bool),
clsarity_bool__Orderings_Opreorder ).
cnf(c_0_122,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| c_HOL_Oord__class_Oless(X1,c_Orderings_Otop__class_Otop(tc_bool),tc_bool)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_109,c_0_110]) ).
cnf(c_0_123,plain,
( ~ c_lessequals(X2,hAPP(c_HOL_Ominus__class_Ominus(X1,tc_bool),X3),tc_bool)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_bool) ),
inference(spm,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_124,plain,
c_lessequals(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2),hAPP(X3,X2),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_113]),c_0_108])]) ).
cnf(c_0_125,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),X2,tc_bool)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_114,c_0_110]) ).
cnf(c_0_126,plain,
( ~ class_Lattices_Olattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3)) = X2 ),
inference(fof_simplification,[status(thm)],[cls_sup__inf__absorb_0]) ).
cnf(c_0_127,axiom,
hAPP(c_COMBB(X1,X2,X3,X4,X5),X6) = hAPP(X1,hAPP(X2,X6)),
cls_COMBB__def_0 ).
cnf(c_0_128,plain,
hAPP(c_Set_Ovimage(X1,X2,X3),X4) = c_COMBB(X4,X1,X3,tc_bool,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_115,c_0_103]),c_0_103]) ).
cnf(c_0_129,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X4))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)) ),
c_0_116 ).
cnf(c_0_130,plain,
hAPP(hAPP(c_in(X1),X2),X3) = hAPP(X3,X2),
inference(spm,[status(thm)],[c_0_117,c_0_118]) ).
cnf(c_0_131,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X2),X3,tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_120]),c_0_121]),c_0_75])]) ).
cnf(c_0_132,plain,
( c_HOL_Oord__class_Oless(X1,c_Orderings_Otop__class_Otop(tc_bool),tc_bool)
| X1 = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_122,c_0_93]) ).
cnf(c_0_133,axiom,
( hBOOL(hAPP(hAPP(c_in(X2),X1),X4))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) ),
cls_vimage__const_1 ).
cnf(c_0_134,plain,
~ c_HOL_Oord__class_Oless(X1,hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X3),tc_bool),
inference(spm,[status(thm)],[c_0_123,c_0_124]) ).
cnf(c_0_135,plain,
( c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),X1,tc_bool)
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_125,c_0_101]) ).
cnf(c_0_136,plain,
( ~ class_Lattices_Olattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3)) = X2 ),
c_0_126 ).
cnf(c_0_137,axiom,
class_Lattices_Olattice(tc_bool),
clsarity_bool__Lattices_Olattice ).
cnf(c_0_138,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X3))
| hAPP(c_Set_Oinsert(X1,X2),X3) = X3 ),
inference(fof_simplification,[status(thm)],[cls_insert__absorb_0]) ).
cnf(c_0_139,plain,
hAPP(hAPP(c_Set_Ovimage(X1,X2,X3),X4),X5) = hAPP(X4,hAPP(X1,X5)),
inference(spm,[status(thm)],[c_0_127,c_0_128]) ).
cnf(c_0_140,plain,
( ~ hBOOL(hAPP(X4,X1))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Otop__class_Otop(tc_fun(X3,tc_bool)) ),
inference(rw,[status(thm)],[c_0_129,c_0_130]) ).
cnf(c_0_141,plain,
hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X2) = c_Orderings_Otop__class_Otop(tc_bool),
inference(spm,[status(thm)],[c_0_131,c_0_132]) ).
cnf(c_0_142,axiom,
hAPP(c_COMBK(X1,X2,X3),X4) = X1,
cls_COMBK__def_0 ).
cnf(c_0_143,plain,
( hBOOL(hAPP(X4,X1))
| hAPP(c_Set_Ovimage(c_COMBK(X1,X2,X3),X3,X2),X4) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) ),
inference(rw,[status(thm)],[c_0_133,c_0_130]) ).
cnf(c_0_144,plain,
hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2) = c_Orderings_Obot__class_Obot(tc_bool),
inference(spm,[status(thm)],[c_0_134,c_0_135]) ).
cnf(c_0_145,axiom,
c_Collect(c_COMBB(c_Not,X1,tc_bool,tc_bool,X2),X2) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X2,tc_bool)),c_Collect(X1,X2)),
cls_Collect__neg__eq_0 ).
cnf(c_0_146,plain,
hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),X2)) = X1,
inference(spm,[status(thm)],[c_0_136,c_0_137]) ).
cnf(c_0_147,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3)) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2),X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X3)) ),
inference(fof_simplification,[status(thm)],[cls_compl__sup_0]) ).
cnf(c_0_148,plain,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3) = X3 ),
inference(fof_simplification,[status(thm)],[cls_le__iff__sup_0]) ).
cnf(c_0_149,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) != hAPP(c_Set_Oinsert(X2,X1),X3),
inference(fof_simplification,[status(thm)],[cls_empty__not__insert_0]) ).
cnf(c_0_150,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X3))
| hAPP(c_Set_Oinsert(X1,X2),X3) = X3 ),
c_0_138 ).
cnf(c_0_151,axiom,
hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_P____),c_Arrow__Order__Mirabelle_OProf)),
cls_CHAINED_0 ).
cnf(c_0_152,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Otop__class_Otop(tc_bool) = hAPP(X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_139,c_0_140]),c_0_141]),c_0_142]) ).
cnf(c_0_153,plain,
( hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_bool) = hAPP(X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_139,c_0_143]),c_0_144]),c_0_142]) ).
cnf(c_0_154,plain,
( ~ hBOOL(hAPP(hAPP(c_Set_Ovimage(X2,X4,X5),X1),X3))
| hBOOL(hAPP(X1,hAPP(X2,X3))) ),
inference(fof_simplification,[status(thm)],[cls_vimage__code_0]) ).
cnf(c_0_155,plain,
c_COMBB(c_Not,X1,tc_bool,tc_bool,X2) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X2,tc_bool)),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_145,c_0_103]),c_0_103]) ).
cnf(c_0_156,plain,
~ c_HOL_Oord__class_Oless(X1,hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),X2),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_146]),c_0_75]),c_0_83])]) ).
cnf(c_0_157,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3)) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2),X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X3)) ),
c_0_147 ).
cnf(c_0_158,plain,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X3) = X3 ),
c_0_148 ).
cnf(c_0_159,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) != hAPP(c_Set_Oinsert(X2,X1),X3),
c_0_149 ).
cnf(c_0_160,plain,
hAPP(c_Set_Oinsert(v_P____,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),c_Arrow__Order__Mirabelle_OProf) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_150,c_0_151]) ).
cnf(c_0_161,plain,
( ~ hBOOL(X1)
| c_Orderings_Otop__class_Otop(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_152,c_0_142]) ).
cnf(c_0_162,plain,
( hBOOL(X1)
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_153,c_0_142]) ).
cnf(c_0_163,plain,
( ~ hBOOL(hAPP(hAPP(c_Set_Ovimage(X2,X4,X5),X1),X3))
| hBOOL(hAPP(X1,hAPP(X2,X3))) ),
c_0_154 ).
cnf(c_0_164,plain,
hAPP(c_Set_Ovimage(X1,X2,tc_bool),c_Not) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X2,tc_bool)),X1),
inference(rw,[status(thm)],[c_0_155,c_0_128]) ).
cnf(c_0_165,axiom,
( hBOOL(hAPP(hAPP(c_in(X1),X2),X3))
| hBOOL(hAPP(hAPP(c_in(X1),X2),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X3))) ),
cls_ComplI_0 ).
cnf(c_0_166,plain,
~ c_HOL_Oord__class_Oless(hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2)),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_156,c_0_157]),c_0_99])]) ).
cnf(c_0_167,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2) = X2 ),
inference(spm,[status(thm)],[c_0_158,c_0_75]) ).
cnf(c_0_168,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),c_Orderings_Otop__class_Otop(X1)) = c_Orderings_Obot__class_Obot(X1) ),
inference(fof_simplification,[status(thm)],[cls_compl__top__eq_0]) ).
cnf(c_0_169,plain,
( ~ class_Lattices_Obounded__lattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(X1),X1),X2) = X2 ),
inference(fof_simplification,[status(thm)],[cls_inf__top__left_0]) ).
cnf(c_0_170,plain,
c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_bool)) != c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_159,c_0_160]) ).
cnf(c_0_171,plain,
( c_Orderings_Otop__class_Otop(tc_bool) = X1
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_161,c_0_162]) ).
cnf(c_0_172,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X3),X2),X1))
| X1 = hAPP(c_Set_Oinsert(X2,X3),c_ATP__Linkup_Osko__Set__Xset__insert__1__1(X1,X2,X3)) ),
inference(fof_simplification,[status(thm)],[cls_set__insert_0]) ).
cnf(c_0_173,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X4),X2))
| ~ hBOOL(hAPP(X3,X4))
| hBOOL(hAPP(hAPP(c_in(X1),c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(X2,X3,X1)),X2)) ),
inference(fof_simplification,[status(thm)],[cls_rev__bexI_0]) ).
cnf(c_0_174,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X3,tc_bool)),X1),X2))
| hBOOL(hAPP(c_Not,hAPP(X1,X2))) ),
inference(spm,[status(thm)],[c_0_163,c_0_164]) ).
cnf(c_0_175,plain,
( hBOOL(hAPP(X2,X3))
| hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X2),X3)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_165,c_0_130]),c_0_130]) ).
cnf(c_0_176,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| ~ c_HOL_Oord__class_Oless(hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X2),tc_bool) ),
inference(spm,[status(thm)],[c_0_166,c_0_167]) ).
cnf(c_0_177,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),c_Orderings_Otop__class_Otop(X1)) = c_Orderings_Obot__class_Obot(X1) ),
c_0_168 ).
cnf(c_0_178,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2)) = X2 ),
inference(fof_simplification,[status(thm)],[cls_double__compl_0]) ).
cnf(c_0_179,plain,
( hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3) != X2
| ~ class_Lattices_Olower__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_le__iff__inf_1]) ).
cnf(c_0_180,plain,
( ~ class_Lattices_Obounded__lattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(X1),X1),X2) = X2 ),
c_0_169 ).
cnf(c_0_181,axiom,
class_Lattices_Obounded__lattice(tc_bool),
clsarity_bool__Lattices_Obounded__lattice ).
cnf(c_0_182,plain,
( ~ class_Orderings_Oorder(X1)
| c_lessequals(X2,X2,X1) ),
inference(fof_simplification,[status(thm)],[cls_order__eq__iff_0]) ).
cnf(c_0_183,plain,
( c_Arrow__Order__Mirabelle_OProf != c_Orderings_Otop__class_Otop(tc_bool)
| c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_bool)) = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_170,c_0_171]) ).
cnf(c_0_184,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X3),X2),X1))
| X1 = hAPP(c_Set_Oinsert(X2,X3),c_ATP__Linkup_Osko__Set__Xset__insert__1__1(X1,X2,X3)) ),
c_0_172 ).
cnf(c_0_185,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X4),X2))
| ~ hBOOL(hAPP(X3,X4))
| hBOOL(hAPP(hAPP(c_in(X1),c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(X2,X3,X1)),X2)) ),
c_0_173 ).
cnf(c_0_186,plain,
( hBOOL(hAPP(X1,X2))
| hBOOL(hAPP(c_Not,hAPP(X1,X2))) ),
inference(spm,[status(thm)],[c_0_174,c_0_175]) ).
cnf(c_0_187,plain,
( ~ c_lessequals(c_Orderings_Otop__class_Otop(tc_bool),X1,tc_bool)
| ~ c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176,c_0_177]),c_0_99])]) ).
cnf(c_0_188,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2)) = X2 ),
c_0_178 ).
cnf(c_0_189,plain,
( hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3) != X2
| ~ class_Lattices_Olower__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
c_0_179 ).
cnf(c_0_190,plain,
hAPP(c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(tc_bool),tc_bool),X1) = X1,
inference(spm,[status(thm)],[c_0_180,c_0_181]) ).
cnf(c_0_191,plain,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1)
| c_lessequals(X3,X2,X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_less__le__not__le_2]) ).
cnf(c_0_192,plain,
( ~ class_Lattices_Obounded__lattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),c_Orderings_Obot__class_Obot(X1)) = X2 ),
inference(fof_simplification,[status(thm)],[cls_sup__bot__right_0]) ).
cnf(c_0_193,plain,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X4),X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_le__supE_0]) ).
cnf(c_0_194,plain,
( ~ class_Orderings_Oorder(X1)
| c_lessequals(X2,X2,X1) ),
c_0_182 ).
cnf(c_0_195,plain,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X4,X1),X2),X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
inference(fof_simplification,[status(thm)],[cls_le__supE_1]) ).
cnf(c_0_196,plain,
( c_Arrow__Order__Mirabelle_OProf != c_Orderings_Otop__class_Otop(tc_bool)
| hAPP(c_Set_Oinsert(X1,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),X2) != c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_159,c_0_183]) ).
cnf(c_0_197,plain,
( ~ hBOOL(hAPP(X3,X1))
| hAPP(c_Set_Oinsert(X1,X2),c_ATP__Linkup_Osko__Set__Xset__insert__1__1(X3,X1,X2)) = X3 ),
inference(rw,[status(thm)],[c_0_184,c_0_130]) ).
cnf(c_0_198,plain,
( ~ hBOOL(hAPP(X2,X4))
| ~ hBOOL(hAPP(X1,X4))
| hBOOL(hAPP(X1,c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(X1,X2,X3))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_185,c_0_130]),c_0_130]) ).
cnf(c_0_199,plain,
( hBOOL(X1)
| hBOOL(hAPP(c_Not,X1)) ),
inference(spm,[status(thm)],[c_0_186,c_0_142]) ).
cnf(c_0_200,axiom,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))) = c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),
cls_Compl__empty__eq_0 ).
cnf(c_0_201,axiom,
hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_bool)),X2)),
cls_top1I_0 ).
cnf(c_0_202,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2)),
inference(fof_simplification,[status(thm)],[cls_bot1E_0]) ).
cnf(c_0_203,plain,
( ~ hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(hAPP(c_in(X1),X2),c_Collect(X3,X1))) ),
inference(fof_simplification,[status(thm)],[cls_CollectI_0]) ).
cnf(c_0_204,plain,
( ~ class_Lattices_Olower__semilattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X3,X1),X2) ),
inference(fof_simplification,[status(thm)],[cls_inf__commute_0]) ).
cnf(c_0_205,plain,
( ~ c_lessequals(c_Orderings_Otop__class_Otop(tc_bool),hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),tc_bool)
| ~ c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),X1,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_187,c_0_188]),c_0_99])]) ).
cnf(c_0_206,plain,
( hAPP(c_HOL_Ominus__class_Ominus(X1,tc_bool),X2) != X1
| c_lessequals(X1,hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X2),tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_112]),c_0_97])]) ).
cnf(c_0_207,plain,
hAPP(c_HOL_Ominus__class_Ominus(c_Orderings_Otop__class_Otop(tc_bool),tc_bool),X1) = hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),
inference(spm,[status(thm)],[c_0_190,c_0_112]) ).
cnf(c_0_208,plain,
( ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1)
| c_lessequals(X3,X2,X1)
| c_HOL_Oord__class_Oless(X2,X3,X1) ),
c_0_191 ).
cnf(c_0_209,plain,
( ~ class_Lattices_Obounded__lattice(X1)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),c_Orderings_Obot__class_Obot(X1)) = X2 ),
c_0_192 ).
cnf(c_0_210,plain,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,X1),X4),X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
c_0_193 ).
cnf(c_0_211,plain,
c_lessequals(X1,X1,tc_bool),
inference(spm,[status(thm)],[c_0_194,c_0_83]) ).
cnf(c_0_212,plain,
( ~ c_lessequals(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X4,X1),X2),X3,X1)
| ~ class_Lattices_Oupper__semilattice(X1)
| c_lessequals(X2,X3,X1) ),
c_0_195 ).
cnf(c_0_213,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),c_Orderings_Obot__class_Obot(X1)) = c_Orderings_Otop__class_Otop(X1) ),
inference(fof_simplification,[status(thm)],[cls_compl__bot__eq_0]) ).
cnf(c_0_214,plain,
( ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_bool),X1))
| c_Arrow__Order__Mirabelle_OProf != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_197])]) ).
cnf(c_0_215,plain,
( ~ hBOOL(hAPP(X1,X3))
| hBOOL(X3)
| hBOOL(hAPP(c_Not,c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(c_Not,X1,X2))) ),
inference(spm,[status(thm)],[c_0_198,c_0_199]) ).
cnf(c_0_216,plain,
hBOOL(hAPP(c_Not,hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_174,c_0_200]),c_0_201])]) ).
cnf(c_0_217,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2)),
c_0_202 ).
cnf(c_0_218,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)),
inference(fof_simplification,[status(thm)],[cls_conjecture_0]) ).
cnf(c_0_219,plain,
( ~ hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(hAPP(c_in(X1),X2),c_Collect(X3,X1))) ),
c_0_203 ).
cnf(c_0_220,plain,
( ~ class_Lattices_Olower__semilattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X3) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X3,X1),X2) ),
c_0_204 ).
cnf(c_0_221,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2)) = c_Orderings_Obot__class_Obot(X1) ),
inference(fof_simplification,[status(thm)],[cls_inf__compl__bot_0]) ).
cnf(c_0_222,plain,
( ~ c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),X1,tc_bool)
| hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_206]),c_0_207]) ).
cnf(c_0_223,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| c_lessequals(X2,X1,tc_bool)
| c_HOL_Oord__class_Oless(X1,X2,tc_bool) ),
inference(spm,[status(thm)],[c_0_208,c_0_121]) ).
cnf(c_0_224,plain,
hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),c_Orderings_Obot__class_Obot(tc_bool)) = X1,
inference(spm,[status(thm)],[c_0_209,c_0_181]) ).
cnf(c_0_225,plain,
c_lessequals(X1,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_210,c_0_211]),c_0_75])]) ).
cnf(c_0_226,plain,
c_lessequals(X1,hAPP(c_Lattices_Oupper__semilattice__class_Osup(X2,tc_bool),X1),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_212,c_0_211]),c_0_75])]) ).
cnf(c_0_227,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_HOL_Ouminus__class_Ouminus(X1),c_Orderings_Obot__class_Obot(X1)) = c_Orderings_Otop__class_Otop(X1) ),
c_0_213 ).
cnf(c_0_228,plain,
( ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_bool),X1))
| c_Arrow__Order__Mirabelle_OProf = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_214,c_0_171]) ).
cnf(c_0_229,plain,
hBOOL(hAPP(c_Not,c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(c_Not,c_Not,X1))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_215,c_0_216]),c_0_217]) ).
cnf(c_0_230,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_Q____),c_Arrow__Order__Mirabelle_OProf)),
c_0_218 ).
cnf(c_0_231,plain,
( ~ hBOOL(hAPP(X3,X2))
| hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
inference(rw,[status(thm)],[c_0_219,c_0_103]) ).
cnf(c_0_232,plain,
hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),X2) = hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,tc_bool),X1),
inference(spm,[status(thm)],[c_0_220,c_0_97]) ).
cnf(c_0_233,plain,
( ~ class_Lattices_Oboolean__algebra(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),hAPP(c_HOL_Ouminus__class_Ouminus(X1),X2)) = c_Orderings_Obot__class_Obot(X1) ),
c_0_221 ).
cnf(c_0_234,plain,
( c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),c_Orderings_Otop__class_Otop(tc_bool),tc_bool)
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_122,c_0_101]) ).
cnf(c_0_235,plain,
( hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1) != c_Orderings_Otop__class_Otop(tc_bool)
| c_lessequals(X1,c_Orderings_Obot__class_Obot(tc_bool),tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_222,c_0_223]),c_0_101])]) ).
cnf(c_0_236,plain,
~ c_HOL_Oord__class_Oless(X1,c_Orderings_Obot__class_Obot(tc_bool),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_224]),c_0_75]),c_0_83])]) ).
cnf(c_0_237,plain,
c_lessequals(X1,hAPP(c_Lattices_Oupper__semilattice__class_Osup(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2),tc_bool),X3),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_210,c_0_225]),c_0_75])]) ).
cnf(c_0_238,plain,
( c_HOL_Oord__class_Oless(X2,c_Orderings_Otop__class_Otop(tc_bool),tc_bool)
| hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2) = X2 ),
inference(spm,[status(thm)],[c_0_122,c_0_226]) ).
cnf(c_0_239,plain,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),c_Orderings_Obot__class_Obot(tc_bool)) = c_Orderings_Otop__class_Otop(tc_bool),
inference(spm,[status(thm)],[c_0_227,c_0_99]) ).
cnf(c_0_240,plain,
( ~ hBOOL(hAPP(X1,X2))
| hBOOL(X1)
| c_Arrow__Order__Mirabelle_OProf = X1 ),
inference(spm,[status(thm)],[c_0_228,c_0_162]) ).
cnf(c_0_241,plain,
hAPP(c_Not,c_ATP__Linkup_Osko__Set__Xrev__bexI__1__1(c_Not,c_Not,X1)) = c_Orderings_Otop__class_Otop(tc_bool),
inference(spm,[status(thm)],[c_0_161,c_0_229]) ).
cnf(c_0_242,plain,
hBOOL(c_Orderings_Otop__class_Otop(tc_bool)),
inference(rw,[status(thm)],[c_0_201,c_0_141]) ).
cnf(c_0_243,negated_conjecture,
~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_Q____)),
inference(spm,[status(thm)],[c_0_230,c_0_231]) ).
cnf(c_0_244,plain,
( hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,tc_bool),X1) != X1
| c_lessequals(X1,X2,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_189,c_0_232]),c_0_97])]) ).
cnf(c_0_245,plain,
hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1)) = c_Orderings_Obot__class_Obot(tc_bool),
inference(spm,[status(thm)],[c_0_233,c_0_99]) ).
cnf(c_0_246,plain,
c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_bool),c_Orderings_Otop__class_Otop(tc_bool),tc_bool),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_234]),c_0_234]) ).
cnf(c_0_247,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_bool)
| hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_235]),c_0_83])]),c_0_236]) ).
cnf(c_0_248,plain,
( ~ c_lessequals(X1,hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X2),tc_bool)
| ~ c_HOL_Oord__class_Oless(hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),X2,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176,c_0_188]),c_0_99])]) ).
cnf(c_0_249,plain,
( c_lessequals(X2,X1,tc_bool)
| c_HOL_Oord__class_Oless(X1,c_Orderings_Otop__class_Otop(tc_bool),tc_bool) ),
inference(spm,[status(thm)],[c_0_237,c_0_238]) ).
cnf(c_0_250,plain,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),c_Orderings_Otop__class_Otop(tc_bool)) = c_Orderings_Obot__class_Obot(tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_239]),c_0_99])]) ).
cnf(c_0_251,plain,
( hBOOL(c_Not)
| c_Not = c_Arrow__Order__Mirabelle_OProf ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_240,c_0_241]),c_0_242])]) ).
cnf(c_0_252,axiom,
hBOOL(hAPP(hAPP(c_fequal(X1),X2),X2)),
cls_ATP__Linkup_Oequal__imp__fequal_0 ).
cnf(c_0_253,negated_conjecture,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_Q____) = c_Orderings_Obot__class_Obot(tc_bool),
inference(spm,[status(thm)],[c_0_243,c_0_153]) ).
cnf(c_0_254,plain,
( hBOOL(X2)
| hBOOL(X1)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_162,c_0_162]) ).
cnf(c_0_255,plain,
( hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1) != c_Orderings_Obot__class_Obot(tc_bool)
| c_lessequals(hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1),X1,tc_bool) ),
inference(spm,[status(thm)],[c_0_244,c_0_245]) ).
cnf(c_0_256,plain,
~ c_lessequals(c_Orderings_Otop__class_Otop(tc_bool),c_Orderings_Obot__class_Obot(tc_bool),tc_bool),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_246]),c_0_121])]) ).
cnf(c_0_257,plain,
( ~ c_HOL_Oord__class_Oless(X3,X2,tc_bool)
| hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,tc_bool),X2)) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_247,c_0_73]),c_0_75])]) ).
cnf(c_0_258,plain,
( ~ c_lessequals(X2,c_Orderings_Obot__class_Obot(tc_bool),tc_bool)
| c_lessequals(X1,hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X2),tc_bool) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_248,c_0_249]),c_0_250]) ).
cnf(c_0_259,plain,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| c_Arrow__Order__Mirabelle_OProf = c_HOL_Ouminus__class_Ouminus(tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_240,c_0_239]),c_0_242])]) ).
cnf(c_0_260,plain,
( c_Not = c_Arrow__Order__Mirabelle_OProf
| c_Not = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_251]) ).
cnf(c_0_261,plain,
hAPP(hAPP(c_fequal(X1),X2),X2) = c_Orderings_Otop__class_Otop(tc_bool),
inference(spm,[status(thm)],[c_0_161,c_0_252]) ).
cnf(c_0_262,negated_conjecture,
( hBOOL(X1)
| hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hAPP(X1,v_Q____) = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_253,c_0_254]) ).
cnf(c_0_263,plain,
c_Orderings_Otop__class_Otop(tc_bool) != c_Orderings_Obot__class_Obot(tc_bool),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_255,c_0_239]),c_0_256]) ).
cnf(c_0_264,plain,
( ~ c_lessequals(X3,X1,tc_bool)
| ~ c_HOL_Oord__class_Oless(X2,X3,tc_bool)
| hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_257,c_0_82]) ).
cnf(c_0_265,plain,
( ~ c_lessequals(hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X2),c_Orderings_Obot__class_Obot(tc_bool),tc_bool)
| c_lessequals(X1,X2,tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_258,c_0_188]),c_0_99])]) ).
cnf(c_0_266,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),v_Q____) = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_253,c_0_259]) ).
cnf(c_0_267,plain,
( c_Arrow__Order__Mirabelle_OProf != c_Orderings_Otop__class_Otop(tc_bool)
| c_Not = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(ef,[status(thm)],[c_0_260]) ).
cnf(c_0_268,axiom,
c_Collect(hAPP(c_fequal(X1),X2),X1) = hAPP(c_Set_Oinsert(X2,X1),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),
cls_singleton__conv2_0 ).
cnf(c_0_269,negated_conjecture,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hBOOL(hAPP(c_fequal(X1),v_Q____)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_261,c_0_262]),c_0_263]) ).
cnf(c_0_270,plain,
~ hBOOL(c_Orderings_Obot__class_Obot(tc_bool)),
inference(rw,[status(thm)],[c_0_217,c_0_144]) ).
cnf(c_0_271,plain,
( ~ c_lessequals(c_Orderings_Otop__class_Otop(tc_bool),X1,tc_bool)
| hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),X1) != c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_264,c_0_246]) ).
cnf(c_0_272,negated_conjecture,
( c_lessequals(X1,v_Q____,tc_bool)
| hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_265,c_0_266]),c_0_211])]) ).
cnf(c_0_273,plain,
( ~ class_Lattices_Olower__semilattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X2) = X2 ),
inference(fof_simplification,[status(thm)],[cls_inf__idem_0]) ).
cnf(c_0_274,plain,
( ~ c_lessequals(X3,X2,X1)
| ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| X2 = X3 ),
inference(fof_simplification,[status(thm)],[cls_order__antisym__conv_0]) ).
cnf(c_0_275,plain,
( c_Arrow__Order__Mirabelle_OProf != c_Orderings_Otop__class_Otop(tc_bool)
| hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_bool),c_Orderings_Obot__class_Obot(tc_bool))) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_216,c_0_267]),c_0_144]) ).
cnf(c_0_276,plain,
hAPP(c_fequal(X1),X2) = hAPP(c_Set_Oinsert(X2,X1),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),
inference(rw,[status(thm)],[c_0_268,c_0_103]) ).
cnf(c_0_277,negated_conjecture,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hBOOL(c_fequal(X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_269,c_0_262]),c_0_270]) ).
cnf(c_0_278,negated_conjecture,
( hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),v_Q____) != c_Orderings_Otop__class_Otop(tc_bool)
| hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool)) ),
inference(spm,[status(thm)],[c_0_271,c_0_272]) ).
cnf(c_0_279,plain,
( ~ class_Lattices_Olower__semilattice(X1)
| hAPP(c_Lattices_Olower__semilattice__class_Oinf(X2,X1),X2) = X2 ),
c_0_273 ).
cnf(c_0_280,plain,
( ~ c_lessequals(X3,X2,X1)
| ~ c_lessequals(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| X2 = X3 ),
c_0_274 ).
cnf(c_0_281,plain,
( hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_Orderings_Obot__class_Obot(tc_bool)))
| c_Arrow__Order__Mirabelle_OProf = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_275,c_0_171])]) ).
cnf(c_0_282,plain,
hAPP(c_fequal(X1),X2) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),
inference(spm,[status(thm)],[c_0_159,c_0_276]) ).
cnf(c_0_283,negated_conjecture,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| c_fequal(X1) = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_277]) ).
cnf(c_0_284,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_bool))) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_254])]) ).
cnf(c_0_285,negated_conjecture,
( hAPP(X1,v_Q____) != c_Orderings_Otop__class_Otop(tc_bool)
| hBOOL(X1)
| hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool)) ),
inference(spm,[status(thm)],[c_0_278,c_0_254]) ).
cnf(c_0_286,plain,
hAPP(c_Lattices_Olower__semilattice__class_Oinf(X1,tc_bool),X1) = X1,
inference(spm,[status(thm)],[c_0_279,c_0_97]) ).
cnf(c_0_287,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| v_Q____ = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_266]),c_0_239]),c_0_99])]) ).
cnf(c_0_288,plain,
( ~ c_lessequals(c_Orderings_Otop__class_Otop(tc_bool),X1,tc_bool)
| c_Orderings_Otop__class_Otop(tc_bool) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_280,c_0_93]),c_0_83])]) ).
cnf(c_0_289,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X2),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X3)))
| ~ hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
inference(fof_simplification,[status(thm)],[cls_ComplD_0]) ).
cnf(c_0_290,plain,
( hBOOL(X1)
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X1))
| c_Arrow__Order__Mirabelle_OProf = X1 ),
inference(spm,[status(thm)],[c_0_281,c_0_162]) ).
cnf(c_0_291,negated_conjecture,
( hAPP(c_Orderings_Otop__class_Otop(tc_bool),X1) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| hBOOL(c_Arrow__Order__Mirabelle_OProf) ),
inference(spm,[status(thm)],[c_0_282,c_0_283]) ).
cnf(c_0_292,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_bool)) = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_284]) ).
cnf(c_0_293,negated_conjecture,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_bool),v_Q____)) ),
inference(spm,[status(thm)],[c_0_269,c_0_283]) ).
cnf(c_0_294,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| c_Arrow__Order__Mirabelle_OProf = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_153,c_0_160]) ).
cnf(c_0_295,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| hBOOL(c_Lattices_Olower__semilattice__class_Oinf(v_Q____,tc_bool)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_285,c_0_286]),c_0_287]) ).
cnf(c_0_296,plain,
( ~ c_lessequals(X1,X2,tc_bool)
| X1 = X2
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_288,c_0_171]) ).
cnf(c_0_297,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X2),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X3)))
| ~ hBOOL(hAPP(hAPP(c_in(X1),X2),X3)) ),
c_0_289 ).
cnf(c_0_298,plain,
( ~ hBOOL(hAPP(X4,hAPP(X1,X5)))
| hBOOL(hAPP(hAPP(c_Set_Ovimage(X1,X2,X3),X4),X5)) ),
inference(fof_simplification,[status(thm)],[cls_vimage__code_1]) ).
cnf(c_0_299,negated_conjecture,
( hBOOL(v_Q____)
| v_Q____ = c_Arrow__Order__Mirabelle_OProf ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_290,c_0_253]),c_0_270]) ).
cnf(c_0_300,negated_conjecture,
( hAPP(c_Orderings_Otop__class_Otop(tc_bool),X1) != c_Orderings_Otop__class_Otop(tc_bool)
| hBOOL(c_Arrow__Order__Mirabelle_OProf) ),
inference(spm,[status(thm)],[c_0_291,c_0_292]) ).
cnf(c_0_301,negated_conjecture,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hAPP(c_Orderings_Otop__class_Otop(tc_bool),v_Q____) = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_293]) ).
cnf(c_0_302,plain,
( c_Arrow__Order__Mirabelle_OProf = c_Orderings_Otop__class_Otop(tc_bool)
| c_Arrow__Order__Mirabelle_OProf = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_294]) ).
cnf(c_0_303,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| c_Lattices_Olower__semilattice__class_Oinf(v_Q____,tc_bool) = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_295]) ).
cnf(c_0_304,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| X1 = v_Q____
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(spm,[status(thm)],[c_0_296,c_0_272]) ).
cnf(c_0_305,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X1),X3),X2))
| ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X2),X3)) ),
inference(spm,[status(thm)],[c_0_297,c_0_231]) ).
cnf(c_0_306,axiom,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X2)) = X2,
cls_double__complement_0 ).
cnf(c_0_307,plain,
( ~ hBOOL(hAPP(X4,hAPP(X1,X5)))
| hBOOL(hAPP(hAPP(c_Set_Ovimage(X1,X2,X3),X4),X5)) ),
c_0_298 ).
cnf(c_0_308,negated_conjecture,
( v_Q____ = c_Arrow__Order__Mirabelle_OProf
| v_Q____ = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_161,c_0_299]) ).
cnf(c_0_309,plain,
hBOOL(hAPP(c_Not,c_Orderings_Obot__class_Obot(tc_bool))),
inference(spm,[status(thm)],[c_0_216,c_0_144]) ).
cnf(c_0_310,negated_conjecture,
hBOOL(c_Arrow__Order__Mirabelle_OProf),
inference(spm,[status(thm)],[c_0_300,c_0_301]) ).
cnf(c_0_311,negated_conjecture,
( c_Arrow__Order__Mirabelle_OProf = c_Orderings_Obot__class_Obot(tc_bool)
| hAPP(c_Orderings_Otop__class_Otop(tc_bool),v_Q____) = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_253,c_0_302]) ).
cnf(c_0_312,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| hAPP(c_Orderings_Otop__class_Otop(tc_bool),v_Q____) = v_Q____ ),
inference(spm,[status(thm)],[c_0_286,c_0_303]) ).
cnf(c_0_313,negated_conjecture,
( v_Q____ != c_Orderings_Obot__class_Obot(tc_bool)
| hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| c_Orderings_Obot__class_Obot(tc_bool) = X1 ),
inference(ef,[status(thm)],[c_0_304]) ).
cnf(c_0_314,plain,
( ~ hBOOL(hAPP(X3,X2))
| ~ hBOOL(hAPP(hAPP(c_in(X1),X2),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X3))) ),
inference(spm,[status(thm)],[c_0_305,c_0_306]) ).
cnf(c_0_315,plain,
( ~ hBOOL(hAPP(c_Not,hAPP(X2,X3)))
| hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X2),X3)) ),
inference(spm,[status(thm)],[c_0_307,c_0_164]) ).
cnf(c_0_316,negated_conjecture,
( v_Q____ = c_Orderings_Otop__class_Otop(tc_bool)
| hAPP(c_Arrow__Order__Mirabelle_OProf,c_Arrow__Order__Mirabelle_OProf) = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_253,c_0_308]) ).
cnf(c_0_317,plain,
hAPP(c_Not,c_Orderings_Obot__class_Obot(tc_bool)) = c_Orderings_Otop__class_Otop(tc_bool),
inference(spm,[status(thm)],[c_0_161,c_0_309]) ).
cnf(c_0_318,negated_conjecture,
c_Arrow__Order__Mirabelle_OProf = c_Orderings_Otop__class_Otop(tc_bool),
inference(spm,[status(thm)],[c_0_161,c_0_310]) ).
cnf(c_0_319,negated_conjecture,
( hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool))
| c_Arrow__Order__Mirabelle_OProf = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_311,c_0_312]),c_0_313]) ).
cnf(c_0_320,plain,
( ~ hBOOL(hAPP(X2,X3))
| ~ hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),X2),X3)) ),
inference(spm,[status(thm)],[c_0_314,c_0_231]) ).
cnf(c_0_321,negated_conjecture,
( hBOOL(hAPP(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(X1,tc_bool)),c_Arrow__Order__Mirabelle_OProf),c_Arrow__Order__Mirabelle_OProf))
| v_Q____ = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_315,c_0_316]),c_0_317]),c_0_242])]) ).
cnf(c_0_322,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_bool),X1)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_214,c_0_318])]) ).
cnf(c_0_323,negated_conjecture,
hBOOL(c_HOL_Ouminus__class_Ouminus(tc_bool)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_319,c_0_318]),c_0_263]) ).
cnf(c_0_324,negated_conjecture,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_Arrow__Order__Mirabelle_OProf))
| v_Q____ = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_320,c_0_321]) ).
cnf(c_0_325,negated_conjecture,
( hBOOL(X1)
| hBOOL(v_Q____)
| X1 = c_Arrow__Order__Mirabelle_OProf ),
inference(spm,[status(thm)],[c_0_299,c_0_254]) ).
cnf(c_0_326,plain,
( ~ hBOOL(hAPP(X1,X2))
| hBOOL(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_322,c_0_254]),c_0_270]) ).
cnf(c_0_327,negated_conjecture,
c_Orderings_Otop__class_Otop(tc_bool) = c_HOL_Ouminus__class_Ouminus(tc_bool),
inference(spm,[status(thm)],[c_0_161,c_0_323]) ).
cnf(c_0_328,negated_conjecture,
( v_Q____ = c_Orderings_Otop__class_Otop(tc_bool)
| hAPP(c_Arrow__Order__Mirabelle_OProf,c_Arrow__Order__Mirabelle_OProf) = c_Arrow__Order__Mirabelle_OProf ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_324,c_0_325]),c_0_161]) ).
cnf(c_0_329,plain,
( ~ hBOOL(X1)
| hBOOL(c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(tc_bool),tc_bool)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_326,c_0_190]),c_0_327]) ).
cnf(c_0_330,negated_conjecture,
( ~ hBOOL(c_Arrow__Order__Mirabelle_OProf)
| v_Q____ = c_Orderings_Otop__class_Otop(tc_bool) ),
inference(spm,[status(thm)],[c_0_324,c_0_328]) ).
cnf(c_0_331,plain,
( ~ hBOOL(X1)
| c_HOL_Ouminus__class_Ouminus(tc_bool) = X1 ),
inference(rw,[status(thm)],[c_0_161,c_0_327]) ).
cnf(c_0_332,negated_conjecture,
hBOOL(c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(tc_bool),tc_bool)),
inference(spm,[status(thm)],[c_0_329,c_0_323]) ).
cnf(c_0_333,negated_conjecture,
( ~ hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hAPP(c_Arrow__Order__Mirabelle_OProf,c_Orderings_Otop__class_Otop(tc_bool)) = c_Orderings_Obot__class_Obot(tc_bool) ),
inference(spm,[status(thm)],[c_0_253,c_0_330]) ).
cnf(c_0_334,negated_conjecture,
c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(tc_bool),tc_bool) = c_HOL_Ouminus__class_Ouminus(tc_bool),
inference(spm,[status(thm)],[c_0_331,c_0_332]) ).
cnf(c_0_335,negated_conjecture,
hAPP(c_HOL_Ouminus__class_Ouminus(tc_bool),c_HOL_Ouminus__class_Ouminus(tc_bool)) = c_Orderings_Obot__class_Obot(tc_bool),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_333,c_0_310])]),c_0_318]),c_0_327]),c_0_327]) ).
cnf(c_0_336,plain,
c_HOL_Ouminus__class_Ouminus(tc_bool) != c_Orderings_Obot__class_Obot(tc_bool),
inference(rw,[status(thm)],[c_0_263,c_0_327]) ).
cnf(c_0_337,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_286,c_0_334]),c_0_335]),c_0_336]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT030-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.08 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.44 % Computer : n016.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 04:31:37 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.51 Running first-order theorem proving
% 0.23/0.52 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.46/4.59 % Version: 3.5.1
% 27.46/4.59 % Preprocessing class: FSLSSMSMSSSNFFN.
% 27.46/4.59 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 27.46/4.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 27.46/4.59 % Starting new_bool_3 with 300s (1) cores
% 27.46/4.59 % Starting new_bool_1 with 300s (1) cores
% 27.46/4.59 % Starting sh5l with 300s (1) cores
% 27.46/4.59 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 1554792 completed with status 0
% 27.46/4.59 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 27.46/4.59 % Preprocessing class: FSLSSMSMSSSNFFN.
% 27.46/4.59 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 27.46/4.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 27.46/4.59 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 27.46/4.59 % No SInE strategy applied
% 27.46/4.59 % Search class: FGHSM-FSLM33-DFFFFFNN
% 27.46/4.59 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 27.46/4.59 % Starting SubtermCWHack with 136s (1) cores
% 27.46/4.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 27.46/4.59 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 27.46/4.59 % Starting G-E--_302_C18_F1_URBAN_S5PRR_RG_S04BN with 136s (1) cores
% 27.46/4.59 % Starting G-E--_208_C09_12_F1_SE_CS_SP_PS_S070I with 136s (1) cores
% 27.46/4.59 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 1554799 completed with status 0
% 27.46/4.59 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 27.46/4.59 % Preprocessing class: FSLSSMSMSSSNFFN.
% 27.46/4.59 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 27.46/4.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 27.46/4.59 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 27.46/4.59 % No SInE strategy applied
% 27.46/4.59 % Search class: FGHSM-FSLM33-DFFFFFNN
% 27.46/4.59 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 27.46/4.59 % Starting SubtermCWHack with 136s (1) cores
% 27.46/4.59 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 27.46/4.59 % Preprocessing time : 0.016 s
% 27.46/4.59 % Presaturation interreduction done
% 27.46/4.59
% 27.46/4.59 % Proof found!
% 27.46/4.59 % SZS status Unsatisfiable
% 27.46/4.59 % SZS output start CNFRefutation
% See solution above
% 27.46/4.59 % Parsed axioms : 701
% 27.46/4.59 % Removed by relevancy pruning/SinE : 0
% 27.46/4.59 % Initial clauses : 701
% 27.46/4.59 % Removed in clause preprocessing : 1
% 27.46/4.59 % Initial clauses in saturation : 700
% 27.46/4.59 % Processed clauses : 8669
% 27.46/4.59 % ...of these trivial : 120
% 27.46/4.59 % ...subsumed : 5863
% 27.46/4.59 % ...remaining for further processing : 2686
% 27.46/4.59 % Other redundant clauses eliminated : 1476
% 27.46/4.59 % Clauses deleted for lack of memory : 0
% 27.46/4.59 % Backward-subsumed : 108
% 27.46/4.59 % Backward-rewritten : 733
% 27.46/4.59 % Generated clauses : 116884
% 27.46/4.59 % ...of the previous two non-redundant : 106809
% 27.46/4.59 % ...aggressively subsumed : 0
% 27.46/4.59 % Contextual simplify-reflections : 14
% 27.46/4.59 % Paramodulations : 115382
% 27.46/4.59 % Factorizations : 18
% 27.46/4.59 % NegExts : 0
% 27.46/4.59 % Equation resolutions : 1484
% 27.46/4.59 % Disequality decompositions : 0
% 27.46/4.59 % Total rewrite steps : 29590
% 27.46/4.59 % ...of those cached : 26472
% 27.46/4.59 % Propositional unsat checks : 0
% 27.46/4.59 % Propositional check models : 0
% 27.46/4.59 % Propositional check unsatisfiable : 0
% 27.46/4.59 % Propositional clauses : 0
% 27.46/4.59 % Propositional clauses after purity: 0
% 27.46/4.59 % Propositional unsat core size : 0
% 27.46/4.59 % Propositional preprocessing time : 0.000
% 27.46/4.59 % Propositional encoding time : 0.000
% 27.46/4.59 % Propositional solver time : 0.000
% 27.46/4.59 % Success case prop preproc time : 0.000
% 27.46/4.59 % Success case prop encoding time : 0.000
% 27.46/4.59 % Success case prop solver time : 0.000
% 27.46/4.59 % Current number of processed clauses : 1287
% 27.46/4.59 % Positive orientable unit clauses : 264
% 27.46/4.59 % Positive unorientable unit clauses: 19
% 27.46/4.59 % Negative unit clauses : 68
% 27.46/4.59 % Non-unit-clauses : 936
% 27.46/4.59 % Current number of unprocessed clauses: 98530
% 27.46/4.59 % ...number of literals in the above : 327993
% 27.46/4.59 % Current number of archived formulas : 0
% 27.46/4.59 % Current number of archived clauses : 1398
% 27.46/4.59 % Clause-clause subsumption calls (NU) : 258446
% 27.46/4.59 % Rec. Clause-clause subsumption calls : 195595
% 27.46/4.59 % Non-unit clause-clause subsumptions : 3748
% 27.46/4.59 % Unit Clause-clause subsumption calls : 8709
% 27.46/4.59 % Rewrite failures with RHS unbound : 0
% 27.46/4.59 % BW rewrite match attempts : 1604
% 27.46/4.59 % BW rewrite match successes : 334
% 27.46/4.59 % Condensation attempts : 0
% 27.46/4.59 % Condensation successes : 0
% 27.46/4.59 % Termbank termtop insertions : 1819720
% 27.46/4.59 % Search garbage collected termcells : 1183
% 27.46/4.59
% 27.46/4.59 % -------------------------------------------------
% 27.46/4.59 % User time : 3.774 s
% 27.46/4.59 % System time : 0.141 s
% 27.46/4.59 % Total time : 3.915 s
% 27.46/4.59 % Maximum resident set size: 4964 pages
% 27.46/4.59
% 27.46/4.59 % -------------------------------------------------
% 27.46/4.59 % User time : 18.752 s
% 27.46/4.59 % System time : 0.633 s
% 27.46/4.59 % Total time : 19.385 s
% 27.46/4.59 % Maximum resident set size: 5120 pages
% 27.46/4.59 % E exiting
%------------------------------------------------------------------------------