%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SCT129+1 : TPTP v9.3.1. Released v5.2.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:55 PM UTC 2026
% Result : ContradictoryAxioms 41.19s 6.69s
% Output : CNFRefutation 41.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 46
% Syntax : Number of formulae : 236 ( 105 unt; 0 def)
% Number of atoms : 456 ( 205 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 399 ( 179 ~; 159 |; 17 &)
% ( 12 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 33 ( 33 usr; 13 con; 0-5 aty)
% Number of variables : 518 ( 76 sgn 261 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_all__not__in__conv,axiom,
! [X7,X5] :
( ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(X5),X3),X7))
<=> X7 = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_all__not__in__conv) ).
fof(fact_DiffE,axiom,
! [X6,X7,X4,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X4),c_Groups_Ominus__class_Ominus(tc_fun(X5,tc_HOL_Obool),X7,X6)))
=> ~ ( hBOOL(hAPP(hAPP(c_member(X5),X4),X7))
=> hBOOL(hAPP(hAPP(c_member(X5),X4),X6)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_DiffE) ).
fof(fact_mem__def,axiom,
! [X7,X12,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X12),X7))
<=> hBOOL(hAPP(X7,X12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mem__def) ).
fof(fact_Un__Diff__Int,axiom,
! [X6,X7,X5] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),c_Groups_Ominus__class_Ominus(tc_fun(X5,tc_HOL_Obool),X7,X6)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X7),X6)) = X7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__Diff__Int) ).
fof(fact_Un__commute,axiom,
! [X6,X7,X5] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),X7),X6) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),X6),X7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__commute) ).
fof(help_c__COMBK__1,axiom,
! [X77,X76,X14,X5] : hAPP(c_COMBK(X5,X14,X76),X77) = X76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__COMBK__1) ).
fof(fact_Un__empty__right,axiom,
! [X7,X5] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),X7),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool))) = X7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__empty__right) ).
fof(fact_Int__lower2,axiom,
! [X6,X7,X5] : c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X7),X6),X6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Int__lower2) ).
fof(fact_le__fun__def,axiom,
! [X1,X2,X5,X14] :
( class_Orderings_Oord(X14)
=> ( c_Orderings_Oord__class_Oless__eq(tc_fun(X5,X14),X2,X1)
<=> ! [X3] : c_Orderings_Oord__class_Oless__eq(X14,hAPP(X2,X3),hAPP(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__fun__def) ).
fof(arity_HOL__Obool__Orderings_Oord,axiom,
class_Orderings_Oord(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Orderings_Oord) ).
fof(fact_fun__upd__same,axiom,
! [X11,X12,X2,X5,X14] : hAPP(c_Fun_Ofun__upd(X14,X5,X2,X12,X11),X12) = X11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_fun__upd__same) ).
fof(fact_inf__absorb1,axiom,
! [X51,X50,X5] :
( class_Lattices_Osemilattice__inf(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X50,X51)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),X51) = X50 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__absorb1) ).
fof(fact_inf__sup__aci_I4_J,axiom,
! [X51,X50,X5] :
( class_Lattices_Olattice(X5)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),X51)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__sup__aci_I4_J) ).
fof(arity_HOL__Obool__Lattices_Osemilattice__inf,axiom,
class_Lattices_Osemilattice__inf(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Lattices_Osemilattice__inf) ).
fof(fact_insert__code,axiom,
! [X12,X7,X11,X5] :
( hBOOL(hAPP(c_Set_Oinsert(X5,X11,X7),X12))
<=> ( hBOOL(hAPP(X7,X12))
| X11 = X12 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__code) ).
fof(arity_HOL__Obool__Lattices_Olattice,axiom,
class_Lattices_Olattice(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Lattices_Olattice) ).
fof(fact_inf__sup__aci_I3_J,axiom,
! [X53,X51,X50,X5] :
( class_Lattices_Olattice(X5)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X51),X53)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X51),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),X53)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__sup__aci_I3_J) ).
fof(fact_inf__absorb2,axiom,
! [X50,X51,X5] :
( class_Lattices_Osemilattice__inf(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X51,X50)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),X51) = X51 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__absorb2) ).
fof(help_c__fequal__2,axiom,
! [X11,X12] :
( hBOOL(hAPP(hAPP(c_fequal,X12),X11))
| X12 != X11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fequal__2) ).
fof(fact_le__infE,axiom,
! [X27,X28,X50,X5] :
( class_Lattices_Osemilattice__inf(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X50,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X28),X27))
=> ~ ( c_Orderings_Oord__class_Oless__eq(X5,X50,X28)
=> ~ c_Orderings_Oord__class_Oless__eq(X5,X50,X27) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__infE) ).
fof(fact_le__iff__inf,axiom,
! [X11,X12,X5] :
( class_Lattices_Osemilattice__inf(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X12,X11)
<=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X12),X11) = X12 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__iff__inf) ).
fof(help_c__fNot__2,axiom,
! [X16] :
( hBOOL(hAPP(c_fNot,X16))
| ~ ~ hBOOL(X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fNot__2) ).
fof(fact_sup__absorb1,axiom,
! [X50,X51,X5] :
( class_Lattices_Osemilattice__sup(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X51,X50)
=> hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X5),X50),X51) = X50 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_sup__absorb1) ).
fof(fact_inf__le1,axiom,
! [X51,X50,X5] :
( class_Lattices_Osemilattice__inf(X5)
=> c_Orderings_Oord__class_Oless__eq(X5,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X50),X51),X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__le1) ).
fof(help_c__fNot__1,axiom,
! [X16] :
( ~ hBOOL(X16)
| ~ hBOOL(hAPP(c_fNot,X16)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fNot__1) ).
fof(fact_split__paired__All,axiom,
! [X14,X5,X16] :
( ! [X18] : hBOOL(hAPP(X16,X18))
<=> ! [X19,X20] : hBOOL(hAPP(X16,hAPP(hAPP(c_Product__Type_OPair(X5,X14),X19),X20))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_split__paired__All) ).
fof(arity_HOL__Obool__Lattices_Osemilattice__sup,axiom,
class_Lattices_Osemilattice__sup(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Lattices_Osemilattice__sup) ).
fof(fact_le__iff__sup,axiom,
! [X11,X12,X5] :
( class_Lattices_Osemilattice__sup(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X12,X11)
<=> hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X5),X12),X11) = X11 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__iff__sup) ).
fof(fact_sup__eq__bot__iff,axiom,
! [X11,X12,X5] :
( class_Lattices_Obounded__lattice__bot(X5)
=> ( hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X5),X12),X11) = c_Orderings_Obot__class_Obot(X5)
<=> ( X11 = c_Orderings_Obot__class_Obot(X5)
& X12 = c_Orderings_Obot__class_Obot(X5) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_sup__eq__bot__iff) ).
fof(fact_disjoint__iff__not__equal,axiom,
! [X6,X7,X5] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X7),X6) = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool))
<=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(X5),X3),X7))
=> ! [X42] :
( hBOOL(hAPP(hAPP(c_member(X5),X42),X6))
=> X3 != X42 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_disjoint__iff__not__equal) ).
fof(fact_bot__apply,axiom,
! [X12,X14,X5] :
( class_Orderings_Obot(X5)
=> hAPP(c_Orderings_Obot__class_Obot(tc_fun(X14,X5)),X12) = c_Orderings_Obot__class_Obot(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_bot__apply) ).
fof(arity_HOL__Obool__Lattices_Obounded__lattice__bot,axiom,
class_Lattices_Obounded__lattice__bot(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Lattices_Obounded__lattice__bot) ).
fof(fact__096F_AQ_A_058_ALin_096,axiom,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,v_Q____)),c_Arrow__Order__Mirabelle_OLin)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096F_AQ_A_058_ALin_096) ).
fof(fact__096P_A_058_AProf_096,axiom,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P____),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096P_A_058_AProf_096) ).
fof(arity_HOL__Obool__Orderings_Obot,axiom,
class_Orderings_Obot(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Orderings_Obot) ).
fof(fact__096P_H_A_058_AProf_096,axiom,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P_H____),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096P_H_A_058_AProf_096) ).
fof(fact_insert__not__empty,axiom,
! [X7,X24,X5] : c_Set_Oinsert(X5,X24,X7) != c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__not__empty) ).
fof(fact_ext,axiom,
! [X1,X2] :
( ! [X3] : hAPP(X2,X3) = hAPP(X1,X3)
=> X2 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ext) ).
fof(fact_Un__insert__right,axiom,
! [X6,X24,X7,X5] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),X7),c_Set_Oinsert(X5,X24,X6)) = c_Set_Oinsert(X5,X24,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),X7),X6)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__insert__right) ).
fof(fact_Int__absorb,axiom,
! [X7,X5] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X7),X7) = X7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Int__absorb) ).
fof(fact_insert__absorb,axiom,
! [X7,X24,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X24),X7))
=> c_Set_Oinsert(X5,X24,X7) = X7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__absorb) ).
fof(fact_calculation,axiom,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_F,v_Q____))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_calculation) ).
fof(fact_Un__empty__left,axiom,
! [X6,X5] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X5,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool))),X6) = X6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__empty__left) ).
fof(fact_eq__mem,axiom,
! [X11,X12,X5] :
( hBOOL(hAPP(hAPP(c_member(X5),X12),hAPP(c_fequal,X11)))
<=> X12 = X11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_eq__mem) ).
fof(fact_Lin__irrefl,axiom,
! [X23,X24,X10] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X10),c_Arrow__Order__Mirabelle_OLin))
=> ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X24),X23)),X10))
=> ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X23),X24)),X10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Lin__irrefl) ).
fof(fact_fun__upd__triv,axiom,
! [X12,X2,X14,X5] : c_Fun_Ofun__upd(X5,X14,X2,X12,hAPP(X2,X12)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_fun__upd__triv) ).
fof(c_0_46,plain,
! [X7,X5] :
( ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(X5),X3),X7))
<=> X7 = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)) ),
inference(fof_simplification,[status(thm)],[fact_all__not__in__conv]) ).
fof(c_0_47,plain,
! [X2138,X2139,X2140,X2141] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X2141),X2140),c_Groups_Ominus__class_Ominus(tc_fun(X2141,tc_HOL_Obool),X2139,X2138)))
| ~ hBOOL(hAPP(hAPP(c_member(X2141),X2140),X2138)) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X2141),X2140),c_Groups_Ominus__class_Ominus(tc_fun(X2141,tc_HOL_Obool),X2139,X2138)))
| hBOOL(hAPP(hAPP(c_member(X2141),X2140),X2139)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_DiffE])])])]) ).
fof(c_0_48,plain,
! [X2073,X2074,X2076,X2077,X2078] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X2077),X2078),X2076))
| X2076 != c_Orderings_Obot__class_Obot(tc_fun(X2077,tc_HOL_Obool)) )
& ( X2073 = c_Orderings_Obot__class_Obot(tc_fun(X2074,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2074),esk99_2(X2073,X2074)),X2073)) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_46])])])])])]) ).
cnf(c_0_49,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X4,X3)))
| ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3)) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_50,plain,
( X2 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X1),esk99_2(X2,X1)),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
fof(c_0_51,plain,
! [X143,X144,X145] :
( ( hBOOL(hAPP(hAPP(c_member(X145),X144),X143))
| ~ hBOOL(hAPP(X143,X144)) )
& ( hBOOL(hAPP(X143,X144))
| ~ hBOOL(hAPP(hAPP(c_member(X145),X144),X143)) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_mem__def])])]) ).
fof(c_0_52,plain,
! [X2150,X2151,X2152] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2152,tc_HOL_Obool)),c_Groups_Ominus__class_Ominus(tc_fun(X2152,tc_HOL_Obool),X2151,X2150)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2152,tc_HOL_Obool)),X2151),X2150)) = X2151,
inference(variable_rename,[status(thm)],[fact_Un__Diff__Int]) ).
fof(c_0_53,plain,
! [X1742,X1743,X1744] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1744,tc_HOL_Obool)),X1743),X1742) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1744,tc_HOL_Obool)),X1742),X1743),
inference(variable_rename,[status(thm)],[fact_Un__commute]) ).
cnf(c_0_54,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),esk99_2(c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,X3),X1)),X3))
| c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
cnf(c_0_55,plain,
( ~ hBOOL(hAPP(X1,X2))
| hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
fof(c_0_56,plain,
! [X2204,X2205,X2206,X2207] : hAPP(c_COMBK(X2207,X2206,X2205),X2204) = X2205,
inference(variable_rename,[status(thm)],[help_c__COMBK__1]) ).
cnf(c_0_57,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,X3)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3)) = X2,
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_58,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),X3) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X3),X2),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_59,plain,
( ~ hBOOL(hAPP(X3,esk99_2(c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,X3),X1)))
| c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_54,c_0_55]) ).
cnf(c_0_60,plain,
hAPP(c_COMBK(X1,X2,X3),X4) = X3,
inference(split_conjunct,[status(thm)],[c_0_56]) ).
fof(c_0_61,plain,
! [X1971,X1972] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1972,tc_HOL_Obool)),X1971),c_Orderings_Obot__class_Obot(tc_fun(X1972,tc_HOL_Obool))) = X1971,
inference(variable_rename,[status(thm)],[fact_Un__empty__right]) ).
fof(c_0_62,plain,
! [X1147,X1148,X1149] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1149,tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1149,tc_HOL_Obool)),X1148),X1147),X1147),
inference(variable_rename,[status(thm)],[fact_Int__lower2]) ).
cnf(c_0_63,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3)),c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,X3)) = X2,
inference(rw,[status(thm)],[c_0_57,c_0_58]) ).
cnf(c_0_64,plain,
( ~ hBOOL(X5)
| c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X2,c_COMBK(X3,X4,X5)) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_65,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))) = X2,
inference(split_conjunct,[status(thm)],[c_0_61]) ).
fof(c_0_66,plain,
! [X1238,X1239,X1240,X1241,X1242] :
( ( ~ class_Orderings_Oord(X1241)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X1240,X1241),X1239,X1238)
| ~ c_Orderings_Oord__class_Oless__eq(X1241,hAPP(X1239,esk74_4(X1238,X1239,X1240,X1241)),hAPP(X1238,esk74_4(X1238,X1239,X1240,X1241))) )
& ( ~ class_Orderings_Oord(X1241)
| c_Orderings_Oord__class_Oless__eq(X1241,hAPP(X1239,X1242),hAPP(X1238,X1242))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X1240,X1241),X1239,X1238) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_le__fun__def])])])])])]) ).
cnf(c_0_67,plain,
c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3),X3),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
cnf(c_0_68,plain,
( ~ hBOOL(X5)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),c_COMBK(X3,X4,X5)) = X2 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_65]) ).
cnf(c_0_69,plain,
( ~ class_Orderings_Oord(X2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X1,X2),X3,X4)
| c_Orderings_Oord__class_Oless__eq(X2,hAPP(X3,X5),hAPP(X4,X5)) ),
inference(split_conjunct,[status(thm)],[c_0_66]) ).
cnf(c_0_70,plain,
( ~ hBOOL(X5)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2,c_COMBK(X3,X4,X5)) ),
inference(spm,[status(thm)],[c_0_67,c_0_68]) ).
cnf(c_0_71,plain,
class_Orderings_Oord(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Oord]) ).
fof(c_0_72,plain,
! [X1595,X1596,X1597,X1598,X1599] : hAPP(c_Fun_Ofun__upd(X1599,X1598,X1597,X1596,X1595),X1596) = X1595,
inference(variable_rename,[status(thm)],[fact_fun__upd__same]) ).
fof(c_0_73,plain,
! [X1098,X1099,X1100] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1100),X1099),X1098) = X1099
| ~ c_Orderings_Oord__class_Oless__eq(X1100,X1099,X1098)
| ~ class_Lattices_Osemilattice__inf(X1100) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__absorb1])])]) ).
cnf(c_0_74,plain,
( ~ hBOOL(X3)
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2),X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_60]),c_0_71])]) ).
cnf(c_0_75,plain,
hAPP(c_Fun_Ofun__upd(X1,X2,X3,X4,X5),X4) = X5,
inference(split_conjunct,[status(thm)],[c_0_72]) ).
fof(c_0_76,plain,
! [X653,X654,X655] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X655),X654),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X655),X654),X653)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X655),X654),X653)
| ~ class_Lattices_Olattice(X655) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__sup__aci_I4_J])])]) ).
cnf(c_0_77,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ class_Lattices_Osemilattice__inf(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),X3) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_78,plain,
( ~ hBOOL(X2)
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,X2) ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_79,plain,
class_Lattices_Osemilattice__inf(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Osemilattice__inf]) ).
fof(c_0_80,plain,
! [X1398,X1399,X1400,X1401] :
( ( hBOOL(hAPP(c_Set_Oinsert(X1401,X1400,X1399),X1398))
| ~ hBOOL(hAPP(X1399,X1398)) )
& ( hBOOL(hAPP(c_Set_Oinsert(X1401,X1400,X1399),X1398))
| X1400 != X1398 )
& ( hBOOL(hAPP(X1399,X1398))
| X1400 = X1398
| ~ hBOOL(hAPP(c_Set_Oinsert(X1401,X1400,X1399),X1398)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_insert__code])])])]) ).
cnf(c_0_81,plain,
( ~ class_Lattices_Olattice(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),X3)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),X3) ),
inference(split_conjunct,[status(thm)],[c_0_76]) ).
cnf(c_0_82,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78]),c_0_79])]) ).
cnf(c_0_83,plain,
class_Lattices_Olattice(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Olattice]) ).
cnf(c_0_84,plain,
( X1 != X2
| hBOOL(hAPP(c_Set_Oinsert(X3,X1,X4),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_80]) ).
fof(c_0_85,plain,
! [X663,X664,X665,X666] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X666),X665),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X666),X664),X663)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X666),X664),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X666),X665),X663))
| ~ class_Lattices_Olattice(X666) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__sup__aci_I3_J])])]) ).
cnf(c_0_86,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X1) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81,c_0_82]),c_0_83])]) ).
cnf(c_0_87,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X2)),
inference(er,[status(thm)],[c_0_84]) ).
fof(c_0_88,plain,
! [X1095,X1096,X1097] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1097),X1095),X1096) = X1096
| ~ c_Orderings_Oord__class_Oless__eq(X1097,X1096,X1095)
| ~ class_Lattices_Osemilattice__inf(X1097) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__absorb2])])]) ).
fof(c_0_89,plain,
! [X11,X12] :
( hBOOL(hAPP(hAPP(c_fequal,X12),X11))
| X12 != X11 ),
inference(fof_simplification,[status(thm)],[help_c__fequal__2]) ).
fof(c_0_90,plain,
! [X27,X28,X50,X5] :
( class_Lattices_Osemilattice__inf(X5)
=> ( c_Orderings_Oord__class_Oless__eq(X5,X50,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X5),X28),X27))
=> ~ ( c_Orderings_Oord__class_Oless__eq(X5,X50,X28)
=> ~ c_Orderings_Oord__class_Oless__eq(X5,X50,X27) ) ) ),
inference(fof_simplification,[status(thm)],[fact_le__infE]) ).
fof(c_0_91,plain,
! [X1113,X1114,X1115] :
( ( ~ class_Lattices_Osemilattice__inf(X1115)
| c_Orderings_Oord__class_Oless__eq(X1115,X1114,X1113)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1115),X1114),X1113) != X1114 )
& ( ~ class_Lattices_Osemilattice__inf(X1115)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1115),X1114),X1113) = X1114
| ~ c_Orderings_Oord__class_Oless__eq(X1115,X1114,X1113) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_le__iff__inf])])])]) ).
cnf(c_0_92,plain,
( ~ class_Lattices_Olattice(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X3),X4)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X3),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),X4)) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
cnf(c_0_93,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X1) = X1,
inference(spm,[status(thm)],[c_0_86,c_0_87]) ).
cnf(c_0_94,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ class_Lattices_Osemilattice__inf(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X3),X2) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
fof(c_0_95,plain,
! [X2228,X2229] :
( hBOOL(hAPP(hAPP(c_fequal,X2229),X2228))
| X2229 != X2228 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_89])]) ).
fof(c_0_96,plain,
! [X1078,X1079,X1080,X1081] :
( ( ~ class_Lattices_Osemilattice__inf(X1081)
| ~ c_Orderings_Oord__class_Oless__eq(X1081,X1080,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1081),X1079),X1078))
| c_Orderings_Oord__class_Oless__eq(X1081,X1080,X1078) )
& ( ~ class_Lattices_Osemilattice__inf(X1081)
| ~ c_Orderings_Oord__class_Oless__eq(X1081,X1080,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1081),X1079),X1078))
| c_Orderings_Oord__class_Oless__eq(X1081,X1080,X1079) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_90])])])]) ).
cnf(c_0_97,plain,
( ~ class_Lattices_Osemilattice__inf(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),X3) != X2
| c_Orderings_Oord__class_Oless__eq(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_91]) ).
cnf(c_0_98,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X2),X1)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X2),X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_93]),c_0_83])]) ).
cnf(c_0_99,plain,
( ~ hBOOL(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2) = X2 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_78]),c_0_79])]) ).
cnf(c_0_100,plain,
( X1 != X2
| hBOOL(hAPP(hAPP(c_fequal,X1),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_95]) ).
fof(c_0_101,plain,
! [X16] :
( hBOOL(hAPP(c_fNot,X16))
| hBOOL(X16) ),
inference(fof_simplification,[status(thm)],[help_c__fNot__2]) ).
fof(c_0_102,plain,
! [X1872,X1873,X1874] :
( hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1874),X1872),X1873) = X1872
| ~ c_Orderings_Oord__class_Oless__eq(X1874,X1873,X1872)
| ~ class_Lattices_Osemilattice__sup(X1874) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_sup__absorb1])])]) ).
cnf(c_0_103,plain,
( ~ class_Lattices_Osemilattice__inf(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X3),X4))
| c_Orderings_Oord__class_Oless__eq(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_96]) ).
cnf(c_0_104,plain,
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X2),X1) != X1
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X2),X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_98]),c_0_79])]) ).
fof(c_0_105,plain,
! [X1122,X1123,X1124] :
( c_Orderings_Oord__class_Oless__eq(X1124,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1124),X1123),X1122),X1123)
| ~ class_Lattices_Osemilattice__inf(X1124) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__le1])])]) ).
fof(c_0_106,plain,
! [X16] :
( ~ hBOOL(X16)
| ~ hBOOL(hAPP(c_fNot,X16)) ),
inference(fof_simplification,[status(thm)],[help_c__fNot__1]) ).
cnf(c_0_107,plain,
( ~ hBOOL(X2)
| ~ hBOOL(X1)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_82,c_0_99]) ).
cnf(c_0_108,plain,
hBOOL(hAPP(hAPP(c_fequal,X1),X1)),
inference(er,[status(thm)],[c_0_100]) ).
fof(c_0_109,plain,
! [X2231] :
( hBOOL(hAPP(c_fNot,X2231))
| hBOOL(X2231) ),
inference(variable_rename,[status(thm)],[c_0_101]) ).
fof(c_0_110,plain,
! [X113,X114,X115,X117,X118,X119,X120,X121,X124] :
( ( hBOOL(hAPP(X121,X124))
| ~ hBOOL(hAPP(X121,hAPP(hAPP(c_Product__Type_OPair(X120,X119),esk4_3(X119,X120,X121)),esk5_3(X119,X120,X121)))) )
& ( hBOOL(hAPP(X115,hAPP(hAPP(c_Product__Type_OPair(X114,X113),X117),X118)))
| ~ hBOOL(hAPP(X115,esk3_3(X113,X114,X115))) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_split__paired__All])])])])])]) ).
cnf(c_0_111,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ class_Lattices_Osemilattice__sup(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1),X3),X2) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
cnf(c_0_112,plain,
class_Lattices_Osemilattice__sup(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Osemilattice__sup]) ).
fof(c_0_113,plain,
! [X1854,X1855,X1856] :
( ( ~ class_Lattices_Osemilattice__sup(X1856)
| c_Orderings_Oord__class_Oless__eq(X1856,X1855,X1854)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1856),X1855),X1854) != X1854 )
& ( ~ class_Lattices_Osemilattice__sup(X1856)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1856),X1855),X1854) = X1854
| ~ c_Orderings_Oord__class_Oless__eq(X1856,X1855,X1854) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_le__iff__sup])])])]) ).
cnf(c_0_114,plain,
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X2),X1) != X1
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103,c_0_104]),c_0_79])]) ).
cnf(c_0_115,plain,
( ~ class_Lattices_Osemilattice__inf(X1)
| c_Orderings_Oord__class_Oless__eq(X1,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1),X2),X3),X2) ),
inference(split_conjunct,[status(thm)],[c_0_105]) ).
fof(c_0_116,plain,
! [X2230] :
( ~ hBOOL(X2230)
| ~ hBOOL(hAPP(c_fNot,X2230)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_106])]) ).
cnf(c_0_117,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = X2 ),
inference(spm,[status(thm)],[c_0_107,c_0_108]) ).
cnf(c_0_118,plain,
( hBOOL(hAPP(c_fNot,X1))
| hBOOL(X1) ),
inference(split_conjunct,[status(thm)],[c_0_109]) ).
cnf(c_0_119,plain,
( ~ hBOOL(hAPP(X1,hAPP(hAPP(c_Product__Type_OPair(X2,X3),esk4_3(X3,X2,X1)),esk5_3(X3,X2,X1))))
| hBOOL(hAPP(X1,X4)) ),
inference(split_conjunct,[status(thm)],[c_0_110]) ).
cnf(c_0_120,plain,
( ~ hBOOL(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X1),X2) = X1 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111,c_0_78]),c_0_112])]) ).
cnf(c_0_121,plain,
( ~ class_Lattices_Osemilattice__sup(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1),X2),X3) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
cnf(c_0_122,plain,
c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2),X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_114,c_0_81]),c_0_83])]) ).
fof(c_0_123,plain,
! [X1975,X1976,X1977] :
( ( ~ class_Lattices_Obounded__lattice__bot(X1977)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1977),X1976),X1975) = c_Orderings_Obot__class_Obot(X1977)
| X1975 != c_Orderings_Obot__class_Obot(X1977)
| X1976 != c_Orderings_Obot__class_Obot(X1977) )
& ( ~ class_Lattices_Obounded__lattice__bot(X1977)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1977),X1976),X1975) != c_Orderings_Obot__class_Obot(X1977)
| X1975 = c_Orderings_Obot__class_Obot(X1977) )
& ( ~ class_Lattices_Obounded__lattice__bot(X1977)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1977),X1976),X1975) != c_Orderings_Obot__class_Obot(X1977)
| X1976 = c_Orderings_Obot__class_Obot(X1977) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_sup__eq__bot__iff])])])]) ).
cnf(c_0_124,plain,
c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2),X2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115,c_0_98]),c_0_79])]) ).
fof(c_0_125,plain,
! [X6,X7,X5] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X5,tc_HOL_Obool)),X7),X6) = c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool))
<=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(X5),X3),X7))
=> ! [X42] :
( hBOOL(hAPP(hAPP(c_member(X5),X42),X6))
=> X3 != X42 ) ) ),
inference(fof_simplification,[status(thm)],[fact_disjoint__iff__not__equal]) ).
cnf(c_0_126,plain,
( ~ hBOOL(X1)
| ~ hBOOL(hAPP(c_fNot,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_116]) ).
cnf(c_0_127,plain,
( hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,X2) ),
inference(spm,[status(thm)],[c_0_117,c_0_118]) ).
cnf(c_0_128,plain,
( ~ hBOOL(X1)
| hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X1),X2)) ),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_129,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2)),X1) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_122]),c_0_112])]) ).
cnf(c_0_130,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| hBOOL(hAPP(X3,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
fof(c_0_131,plain,
! [X2079,X2080,X2081] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2080,X2081)),X2079) = c_Orderings_Obot__class_Obot(X2081)
| ~ class_Orderings_Obot(X2081) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_bot__apply])])]) ).
cnf(c_0_132,plain,
( ~ class_Lattices_Obounded__lattice__bot(X2)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X2),X1),X3) != c_Orderings_Obot__class_Obot(X2)
| X1 = c_Orderings_Obot__class_Obot(X2) ),
inference(split_conjunct,[status(thm)],[c_0_123]) ).
cnf(c_0_133,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2)),X2) = X2,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_124]),c_0_112])]) ).
cnf(c_0_134,plain,
class_Lattices_Obounded__lattice__bot(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Obounded__lattice__bot]) ).
fof(c_0_135,plain,
! [X2048,X2049,X2050,X2051,X2052,X2053,X2054,X2055] :
( ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2055,tc_HOL_Obool)),X2054),X2053) = c_Orderings_Obot__class_Obot(tc_fun(X2055,tc_HOL_Obool))
| esk96_3(X2053,X2054,X2055) = esk97_3(X2053,X2054,X2055) )
& ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2055,tc_HOL_Obool)),X2054),X2053) = c_Orderings_Obot__class_Obot(tc_fun(X2055,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2055),esk97_3(X2053,X2054,X2055)),X2053)) )
& ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2055,tc_HOL_Obool)),X2054),X2053) = c_Orderings_Obot__class_Obot(tc_fun(X2055,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2055),esk96_3(X2053,X2054,X2055)),X2054)) )
& ( X2051 != X2052
| ~ hBOOL(hAPP(hAPP(c_member(X2050),X2052),X2048))
| ~ hBOOL(hAPP(hAPP(c_member(X2050),X2051),X2049))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2050,tc_HOL_Obool)),X2049),X2048) != c_Orderings_Obot__class_Obot(tc_fun(X2050,tc_HOL_Obool)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_125])])])])])])]) ).
cnf(c_0_136,plain,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,v_Q____)),c_Arrow__Order__Mirabelle_OLin)),
inference(split_conjunct,[status(thm)],[fact__096F_AQ_A_058_ALin_096]) ).
cnf(c_0_137,plain,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P____),c_Arrow__Order__Mirabelle_OProf)),
inference(split_conjunct,[status(thm)],[fact__096P_A_058_AProf_096]) ).
cnf(c_0_138,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,hAPP(c_fNot,X2)) ),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
cnf(c_0_139,plain,
( ~ hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2))
| hBOOL(X1) ),
inference(spm,[status(thm)],[c_0_128,c_0_129]) ).
cnf(c_0_140,plain,
( hBOOL(hAPP(X1,esk99_2(X1,X2)))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_130,c_0_50]) ).
cnf(c_0_141,plain,
( ~ class_Orderings_Obot(X1)
| hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2,X1)),X3) = c_Orderings_Obot__class_Obot(X1) ),
inference(split_conjunct,[status(thm)],[c_0_131]) ).
cnf(c_0_142,plain,
class_Orderings_Obot(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Obot]) ).
cnf(c_0_143,plain,
hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P_H____),c_Arrow__Order__Mirabelle_OProf)),
inference(split_conjunct,[status(thm)],[fact__096P_H_A_058_AProf_096]) ).
fof(c_0_144,plain,
! [X7,X24,X5] : c_Set_Oinsert(X5,X24,X7) != c_Orderings_Obot__class_Obot(tc_fun(X5,tc_HOL_Obool)),
inference(fof_simplification,[status(thm)],[fact_insert__not__empty]) ).
fof(c_0_145,plain,
! [X78,X79] :
( X79 = X78
| hAPP(X79,esk1_2(X78,X79)) != hAPP(X78,esk1_2(X78,X79)) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_ext])])])]) ).
cnf(c_0_146,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),c_Orderings_Obot__class_Obot(tc_HOL_Obool)) = c_Orderings_Obot__class_Obot(tc_HOL_Obool),
inference(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132,c_0_133]),c_0_134])])]) ).
cnf(c_0_147,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2)),X1) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_122]),c_0_79])]) ).
cnf(c_0_148,plain,
( X4 != X5
| ~ hBOOL(hAPP(hAPP(c_member(X1),X5),X3))
| ~ hBOOL(hAPP(hAPP(c_member(X1),X4),X2))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(split_conjunct,[status(thm)],[c_0_135]) ).
cnf(c_0_149,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____))),
inference(spm,[status(thm)],[c_0_130,c_0_136]) ).
cnf(c_0_150,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),
inference(spm,[status(thm)],[c_0_130,c_0_137]) ).
cnf(c_0_151,plain,
hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,hAPP(c_fNot,hAPP(hAPP(c_fequal,X2),X2))),
inference(spm,[status(thm)],[c_0_138,c_0_108]) ).
cnf(c_0_152,plain,
( hBOOL(X1)
| hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_139,c_0_140]) ).
cnf(c_0_153,plain,
hAPP(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),X2) = c_Orderings_Obot__class_Obot(tc_HOL_Obool),
inference(spm,[status(thm)],[c_0_141,c_0_142]) ).
cnf(c_0_154,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)),
inference(spm,[status(thm)],[c_0_130,c_0_143]) ).
fof(c_0_155,plain,
! [X1994,X1995,X1996] : c_Set_Oinsert(X1996,X1995,X1994) != c_Orderings_Obot__class_Obot(tc_fun(X1996,tc_HOL_Obool)),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_144])]) ).
fof(c_0_156,plain,
! [X1928,X1929,X1930,X1931] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1931,tc_HOL_Obool)),X1930),c_Set_Oinsert(X1931,X1929,X1928)) = c_Set_Oinsert(X1931,X1929,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1931,tc_HOL_Obool)),X1930),X1928)),
inference(variable_rename,[status(thm)],[fact_Un__insert__right]) ).
cnf(c_0_157,plain,
( hAPP(X1,esk1_2(X2,X1)) != hAPP(X2,esk1_2(X2,X1))
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_145]) ).
cnf(c_0_158,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),c_Orderings_Obot__class_Obot(tc_HOL_Obool)),X1) = c_Orderings_Obot__class_Obot(tc_HOL_Obool),
inference(spm,[status(thm)],[c_0_146,c_0_147]) ).
cnf(c_0_159,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X4),X2))
| ~ hBOOL(hAPP(hAPP(c_member(X1),X4),X3))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(er,[status(thm)],[c_0_148]) ).
fof(c_0_160,plain,
! [X542,X543] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X543,tc_HOL_Obool)),X542),X542) = X542,
inference(variable_rename,[status(thm)],[fact_Int__absorb]) ).
cnf(c_0_161,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)) = X1 ),
inference(spm,[status(thm)],[c_0_107,c_0_149]) ).
cnf(c_0_162,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____) = X1 ),
inference(spm,[status(thm)],[c_0_107,c_0_150]) ).
cnf(c_0_163,plain,
~ hBOOL(hAPP(c_fNot,hAPP(hAPP(c_fequal,X1),X1))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126,c_0_151]),c_0_108])]) ).
cnf(c_0_164,plain,
( hBOOL(X1)
| c_Orderings_Obot__class_Obot(tc_HOL_Obool) = X1 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93,c_0_152]),c_0_153]) ).
cnf(c_0_165,plain,
hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_117,c_0_154]) ).
cnf(c_0_166,plain,
c_Set_Oinsert(X1,X2,X3) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),
inference(split_conjunct,[status(thm)],[c_0_155]) ).
cnf(c_0_167,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),c_Set_Oinsert(X1,X3,X4)) = c_Set_Oinsert(X1,X3,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),X4)),
inference(split_conjunct,[status(thm)],[c_0_156]) ).
fof(c_0_168,plain,
! [X1412,X1413,X1414] :
( c_Set_Oinsert(X1414,X1413,X1412) = X1412
| ~ hBOOL(hAPP(hAPP(c_member(X1414),X1413),X1412)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_insert__absorb])])]) ).
cnf(c_0_169,plain,
( hAPP(X1,esk1_2(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),c_Orderings_Obot__class_Obot(tc_HOL_Obool)),X1)) != c_Orderings_Obot__class_Obot(tc_HOL_Obool)
| X1 = hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),c_Orderings_Obot__class_Obot(tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_157,c_0_158]) ).
cnf(c_0_170,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool))),v_P____),X1))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),tc_HOL_Obool)),X1),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_HOL_Obool)),tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_159,c_0_137]) ).
cnf(c_0_171,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X2) = X2,
inference(split_conjunct,[status(thm)],[c_0_160]) ).
cnf(c_0_172,plain,
hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),
inference(spm,[status(thm)],[c_0_161,c_0_150]) ).
cnf(c_0_173,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_162,c_0_154]) ).
cnf(c_0_174,plain,
c_Orderings_Obot__class_Obot(tc_HOL_Obool) = hAPP(c_fNot,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_163,c_0_164]),c_0_165]) ).
cnf(c_0_175,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),c_Set_Oinsert(X1,X3,X4)) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_166,c_0_167]) ).
cnf(c_0_176,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| c_Set_Oinsert(X1,X2,X3) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_168]) ).
cnf(c_0_177,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(v_F,v_Q____)),X1))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool)),X1),c_Arrow__Order__Mirabelle_OLin) != c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_159,c_0_136]) ).
cnf(c_0_178,plain,
( hAPP(X1,esk1_2(c_COMBK(X2,X3,X4),X1)) != X4
| X1 = c_COMBK(X2,X3,X4) ),
inference(spm,[status(thm)],[c_0_157,c_0_60]) ).
cnf(c_0_179,plain,
c_COMBK(X1,X2,c_Orderings_Obot__class_Obot(tc_HOL_Obool)) = hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),c_Orderings_Obot__class_Obot(tc_HOL_Obool)),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_169,c_0_60])]) ).
cnf(c_0_180,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) = hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),c_Orderings_Obot__class_Obot(tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_169,c_0_153]) ).
cnf(c_0_181,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_HOL_Obool)),tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OProf,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_170,c_0_171]),c_0_137])]) ).
cnf(c_0_182,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_161,c_0_172]),c_0_173]) ).
cnf(c_0_183,plain,
( hBOOL(X1)
| hAPP(c_fNot,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)) = X1 ),
inference(rw,[status(thm)],[c_0_164,c_0_174]) ).
cnf(c_0_184,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X4),X3))
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),X3) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_175,c_0_176]) ).
cnf(c_0_185,plain,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_F,v_Q____))),
inference(split_conjunct,[status(thm)],[fact_calculation]) ).
fof(c_0_186,plain,
! [X1973,X1974] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1974,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X1974,tc_HOL_Obool))),X1973) = X1973,
inference(variable_rename,[status(thm)],[fact_Un__empty__left]) ).
cnf(c_0_187,plain,
c_Orderings_Obot__class_Obot(tc_fun(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool),tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_171]),c_0_136])]) ).
cnf(c_0_188,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) = c_Orderings_Obot__class_Obot(tc_fun(v_a____,tc_HOL_Obool)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_178,c_0_153])]),c_0_179]),c_0_180]) ).
cnf(c_0_189,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_a____,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OProf,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_181,c_0_180]),c_0_180]) ).
cnf(c_0_190,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1
| hAPP(c_fNot,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)) = X1 ),
inference(spm,[status(thm)],[c_0_182,c_0_183]) ).
cnf(c_0_191,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1),hAPP(v_F,v_Q____)) != c_Orderings_Obot__class_Obot(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_184,c_0_185]) ).
cnf(c_0_192,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))),X2) = X2,
inference(split_conjunct,[status(thm)],[c_0_186]) ).
fof(c_0_193,plain,
! [X341,X342,X343] :
( ( hBOOL(hAPP(hAPP(c_member(X343),X342),hAPP(c_fequal,X341)))
| X342 != X341 )
& ( X342 = X341
| ~ hBOOL(hAPP(hAPP(c_member(X343),X342),hAPP(c_fequal,X341))) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_eq__mem])])]) ).
cnf(c_0_194,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_a____,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(rw,[status(thm)],[c_0_187,c_0_188]) ).
cnf(c_0_195,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_189,c_0_188]) ).
cnf(c_0_196,plain,
( X1 = X2
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X2
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(spm,[status(thm)],[c_0_190,c_0_190]) ).
cnf(c_0_197,plain,
c_Orderings_Obot__class_Obot(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)) != hAPP(v_F,v_Q____),
inference(spm,[status(thm)],[c_0_191,c_0_192]) ).
cnf(c_0_198,plain,
( X1 != X2
| hBOOL(hAPP(hAPP(c_member(X3),X1),hAPP(c_fequal,X2))) ),
inference(split_conjunct,[status(thm)],[c_0_193]) ).
cnf(c_0_199,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(spm,[status(thm)],[c_0_194,c_0_188]) ).
cnf(c_0_200,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf
| c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_196])]) ).
cnf(c_0_201,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_a____,tc_HOL_Obool)) != hAPP(v_F,v_Q____),
inference(rw,[status(thm)],[c_0_197,c_0_188]) ).
fof(c_0_202,plain,
! [X23,X24,X10] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X10),c_Arrow__Order__Mirabelle_OLin))
=> ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X24),X23)),X10))
=> ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X23),X24)),X10)) ) ),
inference(fof_simplification,[status(thm)],[fact_Lin__irrefl]) ).
cnf(c_0_203,plain,
hBOOL(hAPP(hAPP(c_member(X1),X2),hAPP(c_fequal,X2))),
inference(er,[status(thm)],[c_0_198]) ).
cnf(c_0_204,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) != c_Arrow__Order__Mirabelle_OLin
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf ),
inference(spm,[status(thm)],[c_0_199,c_0_200]) ).
cnf(c_0_205,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != hAPP(v_F,v_Q____),
inference(spm,[status(thm)],[c_0_201,c_0_188]) ).
fof(c_0_206,plain,
! [X189,X190,X191] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X189),X190)),X191))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X190),X189)),X191))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X191),c_Arrow__Order__Mirabelle_OLin)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_202])])]) ).
cnf(c_0_207,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X3),X2))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),hAPP(c_fequal,X3)) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_159,c_0_203]) ).
cnf(c_0_208,plain,
( c_Arrow__Order__Mirabelle_OLin = X1
| c_Arrow__Order__Mirabelle_OLin = c_Arrow__Order__Mirabelle_OProf
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_204,c_0_196])]) ).
cnf(c_0_209,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) != hAPP(v_F,v_Q____)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf ),
inference(spm,[status(thm)],[c_0_205,c_0_200]) ).
cnf(c_0_210,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3),X2)),X1))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X3)),X1))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X1),c_Arrow__Order__Mirabelle_OLin)) ),
inference(split_conjunct,[status(thm)],[c_0_206]) ).
fof(c_0_211,plain,
! [X1554,X1555,X1556,X1557] : c_Fun_Ofun__upd(X1557,X1556,X1555,X1554,hAPP(X1555,X1554)) = X1555,
inference(variable_rename,[status(thm)],[fact_fun__upd__triv]) ).
cnf(c_0_212,plain,
hAPP(c_fequal,X1) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_207,c_0_171]),c_0_203])]) ).
cnf(c_0_213,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) != c_Arrow__Order__Mirabelle_OProf
| c_Arrow__Order__Mirabelle_OLin = c_Arrow__Order__Mirabelle_OProf ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_208]),c_0_199]) ).
cnf(c_0_214,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1
| hAPP(v_F,v_Q____) = X1
| hAPP(v_F,v_Q____) = c_Arrow__Order__Mirabelle_OProf ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_209,c_0_196])]) ).
cnf(c_0_215,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(c_fequal,hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X1))),c_Arrow__Order__Mirabelle_OLin))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),hAPP(c_fequal,hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X1)))) ),
inference(spm,[status(thm)],[c_0_210,c_0_203]) ).
cnf(c_0_216,plain,
c_Fun_Ofun__upd(X1,X2,X3,X4,hAPP(X3,X4)) = X3,
inference(split_conjunct,[status(thm)],[c_0_211]) ).
cnf(c_0_217,plain,
( hAPP(c_fequal,X1) != hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf ),
inference(spm,[status(thm)],[c_0_212,c_0_200]) ).
cnf(c_0_218,plain,
( hBOOL(X2)
| X1 = X2
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(spm,[status(thm)],[c_0_154,c_0_196]) ).
cnf(c_0_219,plain,
hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(rw,[status(thm)],[c_0_172,c_0_173]) ).
cnf(c_0_220,plain,
c_Arrow__Order__Mirabelle_OLin = c_Arrow__Order__Mirabelle_OProf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_213,c_0_208])]) ).
cnf(c_0_221,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) != c_Arrow__Order__Mirabelle_OProf
| hAPP(v_F,v_Q____) = c_Arrow__Order__Mirabelle_OProf ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_214]),c_0_205]) ).
cnf(c_0_222,plain,
~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),hAPP(c_fequal,hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X1))),c_Arrow__Order__Mirabelle_OLin)),
inference(spm,[status(thm)],[c_0_215,c_0_203]) ).
cnf(c_0_223,plain,
c_Fun_Ofun__upd(X1,X2,c_Arrow__Order__Mirabelle_OProf,v_P____,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_216,c_0_173]) ).
cnf(c_0_224,plain,
( hBOOL(X2)
| hAPP(c_fequal,X1) = X2
| hAPP(c_fequal,X1) = c_Arrow__Order__Mirabelle_OProf ),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_217,c_0_218])]) ).
cnf(c_0_225,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,hAPP(v_F,v_Q____)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(rw,[status(thm)],[c_0_219,c_0_220]) ).
cnf(c_0_226,plain,
hAPP(v_F,v_Q____) = c_Arrow__Order__Mirabelle_OProf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_221,c_0_214])]) ).
cnf(c_0_227,plain,
~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(c_fequal,hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X1)))),
inference(spm,[status(thm)],[c_0_222,c_0_55]) ).
cnf(c_0_228,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hAPP(c_fequal,X1) = c_Arrow__Order__Mirabelle_OProf ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_223,c_0_224]),c_0_223]) ).
cnf(c_0_229,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,c_Arrow__Order__Mirabelle_OProf) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(rw,[status(thm)],[c_0_225,c_0_226]) ).
cnf(c_0_230,plain,
hBOOL(c_Arrow__Order__Mirabelle_OProf),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_227,c_0_228]),c_0_220]),c_0_229]),c_0_154])]) ).
cnf(c_0_231,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_182,c_0_230]) ).
cnf(c_0_232,plain,
( c_Arrow__Order__Mirabelle_OProf = X1
| hAPP(c_fNot,c_Arrow__Order__Mirabelle_OProf) = X1 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_190,c_0_231]),c_0_231]) ).
cnf(c_0_233,plain,
hAPP(c_fequal,X1) != hAPP(c_fNot,c_Arrow__Order__Mirabelle_OProf),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_212,c_0_232]),c_0_195]) ).
cnf(c_0_234,plain,
hAPP(c_fequal,X1) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_233,c_0_232]) ).
cnf(c_0_235,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_227,c_0_234]),c_0_220]),c_0_229]),c_0_231]),c_0_230])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SCT129+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % 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:38:22 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
% 41.19/6.69 % Version: 3.5.1
% 41.19/6.69 % Preprocessing class: FSLSSMSMSSSNFFN.
% 41.19/6.69 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 41.19/6.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 41.19/6.69 % Starting new_bool_3 with 300s (1) cores
% 41.19/6.69 % Starting new_bool_1 with 300s (1) cores
% 41.19/6.69 % Starting sh5l with 300s (1) cores
% 41.19/6.69 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 1562107 completed with status 0
% 41.19/6.69 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 41.19/6.69 % Preprocessing class: FSLSSMSMSSSNFFN.
% 41.19/6.69 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 41.19/6.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 41.19/6.69 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 41.19/6.69 % No SInE strategy applied
% 41.19/6.69 % Search class: FGHSM-FSLM33-DFFFFFNN
% 41.19/6.69 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 41.19/6.69 % Starting SubtermCWHack with 136s (1) cores
% 41.19/6.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 41.19/6.69 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 41.19/6.69 % Starting G-E--_302_C18_F1_URBAN_S5PRR_RG_S04BN with 136s (1) cores
% 41.19/6.69 % Starting G-E--_208_C09_12_F1_SE_CS_SP_PS_S070I with 136s (1) cores
% 41.19/6.69 % U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with pid 1562116 completed with status 0
% 41.19/6.69 % Result found by U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN
% 41.19/6.69 % Preprocessing class: FSLSSMSMSSSNFFN.
% 41.19/6.69 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 41.19/6.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 41.19/6.69 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 41.19/6.69 % No SInE strategy applied
% 41.19/6.69 % Search class: FGHSM-FSLM33-DFFFFFNN
% 41.19/6.69 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 41.19/6.69 % Starting SubtermCWHack with 136s (1) cores
% 41.19/6.69 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 41.19/6.69 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 41.19/6.69 % Preprocessing time : 0.023 s
% 41.19/6.69 % Presaturation interreduction done
% 41.19/6.69
% 41.19/6.69 % Proof found!
% 41.19/6.69 % SZS status ContradictoryAxioms
% 41.19/6.69 % SZS output start CNFRefutation
% See solution above
% 41.19/6.69 % Parsed axioms : 533
% 41.19/6.69 % Removed by relevancy pruning/SinE : 0
% 41.19/6.69 % Initial clauses : 804
% 41.19/6.69 % Removed in clause preprocessing : 38
% 41.19/6.69 % Initial clauses in saturation : 766
% 41.19/6.69 % Processed clauses : 9774
% 41.19/6.69 % ...of these trivial : 261
% 41.19/6.69 % ...subsumed : 6719
% 41.19/6.69 % ...remaining for further processing : 2794
% 41.19/6.69 % Other redundant clauses eliminated : 3123
% 41.19/6.69 % Clauses deleted for lack of memory : 0
% 41.19/6.69 % Backward-subsumed : 104
% 41.19/6.69 % Backward-rewritten : 632
% 41.19/6.69 % Generated clauses : 173726
% 41.19/6.69 % ...of the previous two non-redundant : 161965
% 41.19/6.69 % ...aggressively subsumed : 0
% 41.19/6.69 % Contextual simplify-reflections : 5
% 41.19/6.69 % Paramodulations : 170547
% 41.19/6.69 % Factorizations : 52
% 41.19/6.69 % NegExts : 0
% 41.19/6.69 % Equation resolutions : 3136
% 41.19/6.69 % Disequality decompositions : 0
% 41.19/6.69 % Total rewrite steps : 34941
% 41.19/6.69 % ...of those cached : 32404
% 41.19/6.69 % Propositional unsat checks : 0
% 41.19/6.69 % Propositional check models : 0
% 41.19/6.69 % Propositional check unsatisfiable : 0
% 41.19/6.69 % Propositional clauses : 0
% 41.19/6.69 % Propositional clauses after purity: 0
% 41.19/6.69 % Propositional unsat core size : 0
% 41.19/6.69 % Propositional preprocessing time : 0.000
% 41.19/6.69 % Propositional encoding time : 0.000
% 41.19/6.69 % Propositional solver time : 0.000
% 41.19/6.69 % Success case prop preproc time : 0.000
% 41.19/6.69 % Success case prop encoding time : 0.000
% 41.19/6.69 % Success case prop solver time : 0.000
% 41.19/6.69 % Current number of processed clauses : 1369
% 41.19/6.69 % Positive orientable unit clauses : 230
% 41.19/6.69 % Positive unorientable unit clauses: 15
% 41.19/6.69 % Negative unit clauses : 168
% 41.19/6.69 % Non-unit-clauses : 956
% 41.19/6.69 % Current number of unprocessed clauses: 151802
% 41.19/6.69 % ...number of literals in the above : 528372
% 41.19/6.69 % Current number of archived formulas : 0
% 41.19/6.69 % Current number of archived clauses : 1361
% 41.19/6.69 % Clause-clause subsumption calls (NU) : 263195
% 41.19/6.69 % Rec. Clause-clause subsumption calls : 129811
% 41.19/6.69 % Non-unit clause-clause subsumptions : 3906
% 41.19/6.69 % Unit Clause-clause subsumption calls : 17218
% 41.19/6.69 % Rewrite failures with RHS unbound : 0
% 41.19/6.69 % BW rewrite match attempts : 4847
% 41.19/6.69 % BW rewrite match successes : 349
% 41.19/6.69 % Condensation attempts : 0
% 41.19/6.69 % Condensation successes : 0
% 41.19/6.69 % Termbank termtop insertions : 3784419
% 41.19/6.69 % Search garbage collected termcells : 12449
% 41.19/6.69
% 41.19/6.69 % -------------------------------------------------
% 41.19/6.69 % User time : 5.683 s
% 41.19/6.69 % System time : 0.214 s
% 41.19/6.69 % Total time : 5.897 s
% 41.19/6.69 % Maximum resident set size: 7520 pages
% 41.19/6.69
% 41.19/6.69 % -------------------------------------------------
% 41.19/6.69 % User time : 27.725 s
% 41.19/6.69 % System time : 1.009 s
% 41.19/6.69 % Total time : 28.734 s
% 41.19/6.69 % Maximum resident set size: 5632 pages
% 41.19/6.69 % E exiting
%------------------------------------------------------------------------------