%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SCT134+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:56 PM UTC 2026
% Result : ContradictoryAxioms 25.16s 4.31s
% Output : CNFRefutation 25.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 49
% Syntax : Number of formulae : 255 ( 107 unt; 0 def)
% Number of atoms : 507 ( 218 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 451 ( 199 ~; 183 |; 19 &)
% ( 14 <=>; 36 =>; 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 : 35 ( 35 usr; 13 con; 0-5 aty)
% Number of variables : 564 ( 75 sgn 276 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_all__not__in__conv,axiom,
! [X11,X9] :
( ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(X9),X3),X11))
<=> X11 = c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_all__not__in__conv) ).
fof(fact_insertE,axiom,
! [X11,X22,X23,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X23),c_Set_Oinsert(X9,X22,X11)))
=> ( X23 != X22
=> hBOOL(hAPP(hAPP(c_member(X9),X23),X11)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insertE) ).
fof(fact_ex__in__conv,axiom,
! [X11,X9] :
( ? [X3] : hBOOL(hAPP(hAPP(c_member(X9),X3),X11))
<=> X11 != c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ex__in__conv) ).
fof(fact_insert__not__empty,axiom,
! [X11,X23,X9] : c_Set_Oinsert(X9,X23,X11) != c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__not__empty) ).
fof(fact_DiffE,axiom,
! [X10,X11,X8,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X8),c_Groups_Ominus__class_Ominus(tc_fun(X9,tc_HOL_Obool),X11,X10)))
=> ~ ( hBOOL(hAPP(hAPP(c_member(X9),X8),X11))
=> hBOOL(hAPP(hAPP(c_member(X9),X8),X10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_DiffE) ).
fof(fact_mem__def,axiom,
! [X11,X15,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X15),X11))
<=> hBOOL(hAPP(X11,X15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_mem__def) ).
fof(fact_Un__Diff__Int,axiom,
! [X10,X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),c_Groups_Ominus__class_Ominus(tc_fun(X9,tc_HOL_Obool),X11,X10)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X11),X10)) = X11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__Diff__Int) ).
fof(fact_Un__commute,axiom,
! [X10,X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X11),X10) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X10),X11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__commute) ).
fof(help_c__COMBK__1,axiom,
! [X77,X76,X17,X9] : hAPP(c_COMBK(X9,X17,X76),X77) = X76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__COMBK__1) ).
fof(help_c__COMBI__1,axiom,
! [X76,X9] : hAPP(c_COMBI(X9),X76) = X76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__COMBI__1) ).
fof(fact_Un__empty__right,axiom,
! [X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X11),c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool))) = X11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__empty__right) ).
fof(fact_insert__absorb,axiom,
! [X11,X23,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X23),X11))
=> c_Set_Oinsert(X9,X23,X11) = X11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__absorb) ).
fof(help_c__fequal__2,axiom,
! [X14,X15] :
( hBOOL(hAPP(hAPP(c_fequal,X15),X14))
| X15 != X14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fequal__2) ).
fof(fact_Int__lower2,axiom,
! [X10,X11,X9] : c_Orderings_Oord__class_Oless__eq(tc_fun(X9,tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X11),X10),X10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Int__lower2) ).
fof(fact_le__fun__def,axiom,
! [X1,X2,X9,X17] :
( class_Orderings_Oord(X17)
=> ( c_Orderings_Oord__class_Oless__eq(tc_fun(X9,X17),X2,X1)
<=> ! [X3] : c_Orderings_Oord__class_Oless__eq(X17,hAPP(X2,X3),hAPP(X1,X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__fun__def) ).
fof(fact_le__sup__iff,axiom,
! [X12,X14,X15,X9] :
( class_Lattices_Osemilattice__sup(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X9),X15),X14),X12)
<=> ( c_Orderings_Oord__class_Oless__eq(X9,X14,X12)
& c_Orderings_Oord__class_Oless__eq(X9,X15,X12) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__sup__iff) ).
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_inf__absorb1,axiom,
! [X51,X50,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X50,X51)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X50),X51) = X50 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__absorb1) ).
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_inf__sup__aci_I4_J,axiom,
! [X51,X50,X9] :
( class_Lattices_Olattice(X9)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X50),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X50),X51)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),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(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,X9] :
( class_Lattices_Olattice(X9)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X50),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X51),X53)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X51),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X50),X53)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__sup__aci_I3_J) ).
fof(fact_le__infE,axiom,
! [X26,X27,X50,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X50,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X27),X26))
=> ~ ( c_Orderings_Oord__class_Oless__eq(X9,X50,X27)
=> ~ c_Orderings_Oord__class_Oless__eq(X9,X50,X26) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__infE) ).
fof(fact_le__iff__inf,axiom,
! [X14,X15,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X15,X14)
<=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X15),X14) = X15 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__iff__inf) ).
fof(fact_inf__absorb2,axiom,
! [X50,X51,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X51,X50)
=> hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X50),X51) = X51 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_inf__absorb2) ).
fof(help_c__fNot__2,axiom,
! [X19] :
( hBOOL(hAPP(c_fNot,X19))
| ~ ~ hBOOL(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fNot__2) ).
fof(fact_sup__absorb1,axiom,
! [X50,X51,X9] :
( class_Lattices_Osemilattice__sup(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X51,X50)
=> hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X9),X50),X51) = X50 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_sup__absorb1) ).
fof(fact_le__iff__sup,axiom,
! [X14,X15,X9] :
( class_Lattices_Osemilattice__sup(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X15,X14)
<=> hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X9),X15),X14) = X14 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__iff__sup) ).
fof(help_c__fNot__1,axiom,
! [X19] :
( ~ hBOOL(X19)
| ~ hBOOL(hAPP(c_fNot,X19)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fNot__1) ).
fof(fact_split__paired__All,axiom,
! [X17,X9,X19] :
( ! [X21] : hBOOL(hAPP(X19,X21))
<=> ! [X6,X7] : hBOOL(hAPP(X19,hAPP(hAPP(c_Product__Type_OPair(X9,X17),X6),X7))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_split__paired__All) ).
fof(fact_sup__eq__bot__iff,axiom,
! [X14,X15,X9] :
( class_Lattices_Obounded__lattice__bot(X9)
=> ( hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X9),X15),X14) = c_Orderings_Obot__class_Obot(X9)
<=> ( X14 = c_Orderings_Obot__class_Obot(X9)
& X15 = c_Orderings_Obot__class_Obot(X9) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_sup__eq__bot__iff) ).
fof(fact_disjoint__iff__not__equal,axiom,
! [X10,X11,X9] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X11),X10) = c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool))
<=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(X9),X3),X11))
=> ! [X5] :
( hBOOL(hAPP(hAPP(c_member(X9),X5),X10))
=> X3 != X5 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_disjoint__iff__not__equal) ).
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(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_bot__apply,axiom,
! [X15,X17,X9] :
( class_Orderings_Obot(X9)
=> hAPP(c_Orderings_Obot__class_Obot(tc_fun(X17,X9)),X15) = c_Orderings_Obot__class_Obot(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_bot__apply) ).
fof(fact_emptyE,axiom,
! [X23,X9] : ~ hBOOL(hAPP(hAPP(c_member(X9),X23),c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_emptyE) ).
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__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_Int__absorb,axiom,
! [X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X11),X11) = X11,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Int__absorb) ).
fof(fact_Un__insert__right,axiom,
! [X10,X23,X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X11),c_Set_Oinsert(X9,X23,X10)) = c_Set_Oinsert(X9,X23,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X11),X10)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__insert__right) ).
fof(fact__096Q_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_Q____),c_Arrow__Order__Mirabelle_OProf)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096Q_A_058_AProf_096) ).
fof(fact__096a_H_A_060_092_060_094bsub_062F_AQ_092_060_094esub_062_Ab_H_096,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_H____),v_b_H____)),hAPP(v_F,v_Q____))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096a_H_A_060_092_060_094bsub_062F_AQ_092_060_094esub_062_Ab_H_096) ).
fof(fact_Un__empty__left,axiom,
! [X10,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool))),X10) = X10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Un__empty__left) ).
fof(fact_eq__mem,axiom,
! [X14,X15,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X15),hAPP(c_fequal,X14)))
<=> X15 = X14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_eq__mem) ).
fof(fact_Lin__irrefl,axiom,
! [X22,X23,X13] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X13),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),X23),X22)),X13))
=> ~ 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),X22),X23)),X13)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Lin__irrefl) ).
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(fact_fun__upd__triv,axiom,
! [X15,X2,X17,X9] : c_Fun_Ofun__upd(X9,X17,X2,X15,hAPP(X2,X15)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_fun__upd__triv) ).
fof(c_0_49,plain,
! [X11,X9] :
( ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(X9),X3),X11))
<=> X11 = c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)) ),
inference(fof_simplification,[status(thm)],[fact_all__not__in__conv]) ).
fof(c_0_50,plain,
! [X11,X22,X23,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X23),c_Set_Oinsert(X9,X22,X11)))
=> ( X23 != X22
=> hBOOL(hAPP(hAPP(c_member(X9),X23),X11)) ) ),
inference(fof_simplification,[status(thm)],[fact_insertE]) ).
fof(c_0_51,plain,
! [X11,X9] :
( ? [X3] : hBOOL(hAPP(hAPP(c_member(X9),X3),X11))
<=> X11 != c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)) ),
inference(fof_simplification,[status(thm)],[fact_ex__in__conv]) ).
fof(c_0_52,plain,
! [X11,X23,X9] : c_Set_Oinsert(X9,X23,X11) != c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)),
inference(fof_simplification,[status(thm)],[fact_insert__not__empty]) ).
fof(c_0_53,plain,
! [X2140,X2141,X2142,X2143] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X2143),X2142),c_Groups_Ominus__class_Ominus(tc_fun(X2143,tc_HOL_Obool),X2141,X2140)))
| ~ hBOOL(hAPP(hAPP(c_member(X2143),X2142),X2140)) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X2143),X2142),c_Groups_Ominus__class_Ominus(tc_fun(X2143,tc_HOL_Obool),X2141,X2140)))
| hBOOL(hAPP(hAPP(c_member(X2143),X2142),X2141)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_DiffE])])])]) ).
fof(c_0_54,plain,
! [X2075,X2076,X2078,X2079,X2080] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X2079),X2080),X2078))
| X2078 != c_Orderings_Obot__class_Obot(tc_fun(X2079,tc_HOL_Obool)) )
& ( X2075 = c_Orderings_Obot__class_Obot(tc_fun(X2076,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2076),esk100_2(X2075,X2076)),X2075)) ) ),
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_49])])])])])]) ).
fof(c_0_55,plain,
! [X1374,X1375,X1376,X1377] :
( hBOOL(hAPP(hAPP(c_member(X1377),X1376),X1374))
| X1376 = X1375
| ~ hBOOL(hAPP(hAPP(c_member(X1377),X1376),c_Set_Oinsert(X1377,X1375,X1374))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_50])])]) ).
fof(c_0_56,plain,
! [X2069,X2070,X2071,X2072,X2073] :
( ( hBOOL(hAPP(hAPP(c_member(X2073),esk99_2(X2072,X2073)),X2072))
| X2072 = c_Orderings_Obot__class_Obot(tc_fun(X2073,tc_HOL_Obool)) )
& ( X2069 != c_Orderings_Obot__class_Obot(tc_fun(X2070,tc_HOL_Obool))
| ~ hBOOL(hAPP(hAPP(c_member(X2070),X2071),X2069)) ) ),
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_51])])])])])]) ).
fof(c_0_57,plain,
! [X1998,X1999,X2000] : c_Set_Oinsert(X2000,X1999,X1998) != c_Orderings_Obot__class_Obot(tc_fun(X2000,tc_HOL_Obool)),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_52])]) ).
cnf(c_0_58,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_53]) ).
cnf(c_0_59,plain,
( X2 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X1),esk100_2(X2,X1)),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
fof(c_0_60,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])])]) ).
cnf(c_0_61,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),c_Set_Oinsert(X1,X3,X4)))
| hBOOL(hAPP(hAPP(c_member(X1),X2),X4))
| X2 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
cnf(c_0_62,plain,
( hBOOL(hAPP(hAPP(c_member(X2),esk99_2(X1,X2)),X1))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_63,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_57]) ).
fof(c_0_64,plain,
! [X2152,X2153,X2154] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2154,tc_HOL_Obool)),c_Groups_Ominus__class_Ominus(tc_fun(X2154,tc_HOL_Obool),X2153,X2152)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2154,tc_HOL_Obool)),X2153),X2152)) = X2153,
inference(variable_rename,[status(thm)],[fact_Un__Diff__Int]) ).
fof(c_0_65,plain,
! [X1714,X1715,X1716] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1716,tc_HOL_Obool)),X1715),X1714) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1716,tc_HOL_Obool)),X1714),X1715),
inference(variable_rename,[status(thm)],[fact_Un__commute]) ).
cnf(c_0_66,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),esk100_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_58,c_0_59]) ).
cnf(c_0_67,plain,
( ~ hBOOL(hAPP(X1,X2))
| hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
fof(c_0_68,plain,
! [X2199,X2200,X2201,X2202] : hAPP(c_COMBK(X2202,X2201,X2200),X2199) = X2200,
inference(variable_rename,[status(thm)],[help_c__COMBK__1]) ).
cnf(c_0_69,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| hBOOL(hAPP(X3,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_70,plain,
( hBOOL(hAPP(hAPP(c_member(X1),esk99_2(c_Set_Oinsert(X1,X2,X3),X1)),X3))
| esk99_2(c_Set_Oinsert(X1,X2,X3),X1) = X2 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_62]),c_0_63]) ).
fof(c_0_71,plain,
! [X2197,X2198] : hAPP(c_COMBI(X2198),X2197) = X2197,
inference(variable_rename,[status(thm)],[help_c__COMBI__1]) ).
cnf(c_0_72,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_64]) ).
cnf(c_0_73,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_65]) ).
cnf(c_0_74,plain,
( ~ hBOOL(hAPP(X3,esk100_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_66,c_0_67]) ).
cnf(c_0_75,plain,
hAPP(c_COMBK(X1,X2,X3),X4) = X3,
inference(split_conjunct,[status(thm)],[c_0_68]) ).
fof(c_0_76,plain,
! [X1973,X1974] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1974,tc_HOL_Obool)),X1973),c_Orderings_Obot__class_Obot(tc_fun(X1974,tc_HOL_Obool))) = X1973,
inference(variable_rename,[status(thm)],[fact_Un__empty__right]) ).
cnf(c_0_77,plain,
( hBOOL(hAPP(X3,esk99_2(c_Set_Oinsert(X1,X2,X3),X1)))
| esk99_2(c_Set_Oinsert(X1,X2,X3),X1) = X2 ),
inference(spm,[status(thm)],[c_0_69,c_0_70]) ).
cnf(c_0_78,plain,
hAPP(c_COMBI(X1),X2) = X2,
inference(split_conjunct,[status(thm)],[c_0_71]) ).
fof(c_0_79,plain,
! [X1399,X1400,X1401] :
( c_Set_Oinsert(X1401,X1400,X1399) = X1399
| ~ hBOOL(hAPP(hAPP(c_member(X1401),X1400),X1399)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_insert__absorb])])]) ).
fof(c_0_80,plain,
! [X14,X15] :
( hBOOL(hAPP(hAPP(c_fequal,X15),X14))
| X15 != X14 ),
inference(fof_simplification,[status(thm)],[help_c__fequal__2]) ).
fof(c_0_81,plain,
! [X1151,X1152,X1153] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1153,tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1153,tc_HOL_Obool)),X1152),X1151),X1151),
inference(variable_rename,[status(thm)],[fact_Int__lower2]) ).
cnf(c_0_82,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_72,c_0_73]) ).
cnf(c_0_83,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_74,c_0_75]) ).
cnf(c_0_84,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_76]) ).
cnf(c_0_85,plain,
( hBOOL(hAPP(hAPP(c_member(X1),esk100_2(c_Set_Oinsert(X1,X2,X3),X1)),X3))
| esk100_2(c_Set_Oinsert(X1,X2,X3),X1) = X2 ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_59]),c_0_63]) ).
cnf(c_0_86,plain,
( hBOOL(esk99_2(c_Set_Oinsert(X1,X2,c_COMBI(X3)),X1))
| esk99_2(c_Set_Oinsert(X1,X2,c_COMBI(X3)),X1) = X2 ),
inference(spm,[status(thm)],[c_0_77,c_0_78]) ).
cnf(c_0_87,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| c_Set_Oinsert(X1,X2,X3) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_79]) ).
fof(c_0_88,plain,
! [X2223,X2224] :
( hBOOL(hAPP(hAPP(c_fequal,X2224),X2223))
| X2224 != X2223 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_80])]) ).
fof(c_0_89,plain,
! [X1242,X1243,X1244,X1245,X1246] :
( ( ~ class_Orderings_Oord(X1245)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X1244,X1245),X1243,X1242)
| ~ c_Orderings_Oord__class_Oless__eq(X1245,hAPP(X1243,esk75_4(X1242,X1243,X1244,X1245)),hAPP(X1242,esk75_4(X1242,X1243,X1244,X1245))) )
& ( ~ class_Orderings_Oord(X1245)
| c_Orderings_Oord__class_Oless__eq(X1245,hAPP(X1243,X1246),hAPP(X1242,X1246))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X1244,X1245),X1243,X1242) ) ),
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_90,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_81]) ).
cnf(c_0_91,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_82,c_0_83]),c_0_84]) ).
cnf(c_0_92,plain,
( hBOOL(hAPP(X3,esk100_2(c_Set_Oinsert(X1,X2,X3),X1)))
| esk100_2(c_Set_Oinsert(X1,X2,X3),X1) = X2 ),
inference(spm,[status(thm)],[c_0_69,c_0_85]) ).
cnf(c_0_93,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X2),X3),c_COMBI(X1)))
| hBOOL(esk99_2(c_COMBI(X1),X2))
| esk99_2(c_COMBI(X1),X2) = X3 ),
inference(spm,[status(thm)],[c_0_86,c_0_87]) ).
cnf(c_0_94,plain,
( X1 != X2
| hBOOL(hAPP(hAPP(c_fequal,X1),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
fof(c_0_95,plain,
! [X1859,X1860,X1861,X1862] :
( ( ~ class_Lattices_Osemilattice__sup(X1862)
| c_Orderings_Oord__class_Oless__eq(X1862,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1862),X1861),X1860),X1859)
| ~ c_Orderings_Oord__class_Oless__eq(X1862,X1860,X1859)
| ~ c_Orderings_Oord__class_Oless__eq(X1862,X1861,X1859) )
& ( ~ class_Lattices_Osemilattice__sup(X1862)
| ~ c_Orderings_Oord__class_Oless__eq(X1862,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1862),X1861),X1860),X1859)
| c_Orderings_Oord__class_Oless__eq(X1862,X1860,X1859) )
& ( ~ class_Lattices_Osemilattice__sup(X1862)
| ~ c_Orderings_Oord__class_Oless__eq(X1862,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1862),X1861),X1860),X1859)
| c_Orderings_Oord__class_Oless__eq(X1862,X1861,X1859) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_le__sup__iff])])])]) ).
cnf(c_0_96,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_89]) ).
cnf(c_0_97,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_90,c_0_91]) ).
cnf(c_0_98,plain,
class_Orderings_Oord(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Oord]) ).
cnf(c_0_99,plain,
( hBOOL(esk100_2(c_Set_Oinsert(X1,X2,c_COMBI(X3)),X1))
| esk100_2(c_Set_Oinsert(X1,X2,c_COMBI(X3)),X1) = X2 ),
inference(spm,[status(thm)],[c_0_92,c_0_78]) ).
cnf(c_0_100,plain,
( ~ hBOOL(X3)
| hBOOL(esk99_2(c_COMBI(X1),X2))
| esk99_2(c_COMBI(X1),X2) = X3 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93,c_0_67]),c_0_78]) ).
cnf(c_0_101,plain,
hBOOL(hAPP(hAPP(c_fequal,X1),X1)),
inference(er,[status(thm)],[c_0_94]) ).
fof(c_0_102,plain,
! [X1102,X1103,X1104] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1104),X1103),X1102) = X1103
| ~ c_Orderings_Oord__class_Oless__eq(X1104,X1103,X1102)
| ~ class_Lattices_Osemilattice__inf(X1104) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__absorb1])])]) ).
cnf(c_0_103,plain,
( ~ class_Lattices_Osemilattice__sup(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1),X2),X4),X3)
| c_Orderings_Oord__class_Oless__eq(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_95]) ).
cnf(c_0_104,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_96,c_0_97]),c_0_75]),c_0_98])]) ).
cnf(c_0_105,plain,
class_Lattices_Osemilattice__sup(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Osemilattice__sup]) ).
cnf(c_0_106,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X2),X3),c_COMBI(X1)))
| hBOOL(esk100_2(c_COMBI(X1),X2))
| esk100_2(c_COMBI(X1),X2) = X3 ),
inference(spm,[status(thm)],[c_0_99,c_0_87]) ).
cnf(c_0_107,plain,
( hBOOL(esk99_2(c_COMBI(X1),X2))
| esk99_2(c_COMBI(X1),X2) = hAPP(hAPP(c_fequal,X3),X3) ),
inference(spm,[status(thm)],[c_0_100,c_0_101]) ).
fof(c_0_108,plain,
! [X670,X671,X672] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X672),X671),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X672),X671),X670)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X672),X671),X670)
| ~ class_Lattices_Olattice(X672) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__sup__aci_I4_J])])]) ).
cnf(c_0_109,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_102]) ).
cnf(c_0_110,plain,
( ~ hBOOL(X2)
| 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_105])]) ).
cnf(c_0_111,plain,
class_Lattices_Osemilattice__inf(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Osemilattice__inf]) ).
cnf(c_0_112,plain,
( ~ hBOOL(X3)
| hBOOL(esk100_2(c_COMBI(X1),X2))
| esk100_2(c_COMBI(X1),X2) = X3 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_67]),c_0_78]) ).
cnf(c_0_113,plain,
hBOOL(esk99_2(c_COMBI(X1),X2)),
inference(spm,[status(thm)],[c_0_101,c_0_107]) ).
cnf(c_0_114,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_108]) ).
cnf(c_0_115,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_109,c_0_110]),c_0_111])]) ).
cnf(c_0_116,plain,
class_Lattices_Olattice(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Olattice]) ).
cnf(c_0_117,plain,
( hBOOL(esk100_2(c_COMBI(X1),X2))
| esk100_2(c_COMBI(X1),X2) = esk99_2(c_COMBI(X3),X4) ),
inference(spm,[status(thm)],[c_0_112,c_0_113]) ).
fof(c_0_118,plain,
! [X680,X681,X682,X683] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X683),X682),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X683),X681),X680)) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X683),X681),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X683),X682),X680))
| ~ class_Lattices_Olattice(X683) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__sup__aci_I3_J])])]) ).
cnf(c_0_119,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_114,c_0_115]),c_0_116])]) ).
cnf(c_0_120,plain,
hBOOL(esk100_2(c_COMBI(X1),X2)),
inference(spm,[status(thm)],[c_0_113,c_0_117]) ).
fof(c_0_121,plain,
! [X26,X27,X50,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X50,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X27),X26))
=> ~ ( c_Orderings_Oord__class_Oless__eq(X9,X50,X27)
=> ~ c_Orderings_Oord__class_Oless__eq(X9,X50,X26) ) ) ),
inference(fof_simplification,[status(thm)],[fact_le__infE]) ).
fof(c_0_122,plain,
! [X1117,X1118,X1119] :
( ( ~ class_Lattices_Osemilattice__inf(X1119)
| c_Orderings_Oord__class_Oless__eq(X1119,X1118,X1117)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1119),X1118),X1117) != X1118 )
& ( ~ class_Lattices_Osemilattice__inf(X1119)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1119),X1118),X1117) = X1118
| ~ c_Orderings_Oord__class_Oless__eq(X1119,X1118,X1117) ) ),
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_123,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_118]) ).
cnf(c_0_124,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X1) = X1,
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
fof(c_0_125,plain,
! [X1099,X1100,X1101] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1101),X1099),X1100) = X1100
| ~ c_Orderings_Oord__class_Oless__eq(X1101,X1100,X1099)
| ~ class_Lattices_Osemilattice__inf(X1101) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__absorb2])])]) ).
fof(c_0_126,plain,
! [X1082,X1083,X1084,X1085] :
( ( ~ class_Lattices_Osemilattice__inf(X1085)
| ~ c_Orderings_Oord__class_Oless__eq(X1085,X1084,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1085),X1083),X1082))
| c_Orderings_Oord__class_Oless__eq(X1085,X1084,X1082) )
& ( ~ class_Lattices_Osemilattice__inf(X1085)
| ~ c_Orderings_Oord__class_Oless__eq(X1085,X1084,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1085),X1083),X1082))
| c_Orderings_Oord__class_Oless__eq(X1085,X1084,X1083) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_121])])])]) ).
cnf(c_0_127,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_122]) ).
cnf(c_0_128,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_123,c_0_124]),c_0_116])]) ).
cnf(c_0_129,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_125]) ).
cnf(c_0_130,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_126]) ).
cnf(c_0_131,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_127,c_0_128]),c_0_111])]) ).
cnf(c_0_132,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_129,c_0_110]),c_0_111])]) ).
fof(c_0_133,plain,
! [X19] :
( hBOOL(hAPP(c_fNot,X19))
| hBOOL(X19) ),
inference(fof_simplification,[status(thm)],[help_c__fNot__2]) ).
fof(c_0_134,plain,
! [X1874,X1875,X1876] :
( hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1876),X1874),X1875) = X1874
| ~ c_Orderings_Oord__class_Oless__eq(X1876,X1875,X1874)
| ~ class_Lattices_Osemilattice__sup(X1876) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_sup__absorb1])])]) ).
fof(c_0_135,plain,
! [X1856,X1857,X1858] :
( ( ~ class_Lattices_Osemilattice__sup(X1858)
| c_Orderings_Oord__class_Oless__eq(X1858,X1857,X1856)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1858),X1857),X1856) != X1856 )
& ( ~ class_Lattices_Osemilattice__sup(X1858)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1858),X1857),X1856) = X1856
| ~ c_Orderings_Oord__class_Oless__eq(X1858,X1857,X1856) ) ),
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_136,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_130,c_0_131]),c_0_111])]) ).
fof(c_0_137,plain,
! [X19] :
( ~ hBOOL(X19)
| ~ hBOOL(hAPP(c_fNot,X19)) ),
inference(fof_simplification,[status(thm)],[help_c__fNot__1]) ).
cnf(c_0_138,plain,
( ~ hBOOL(X2)
| ~ hBOOL(X1)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_115,c_0_132]) ).
fof(c_0_139,plain,
! [X2226] :
( hBOOL(hAPP(c_fNot,X2226))
| hBOOL(X2226) ),
inference(variable_rename,[status(thm)],[c_0_133]) ).
fof(c_0_140,plain,
! [X118,X119,X120,X122,X123,X124,X125,X126,X129] :
( ( hBOOL(hAPP(X126,X129))
| ~ hBOOL(hAPP(X126,hAPP(hAPP(c_Product__Type_OPair(X125,X124),esk5_3(X124,X125,X126)),esk6_3(X124,X125,X126)))) )
& ( hBOOL(hAPP(X120,hAPP(hAPP(c_Product__Type_OPair(X119,X118),X122),X123)))
| ~ hBOOL(hAPP(X120,esk4_3(X118,X119,X120))) ) ),
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_141,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_134]) ).
fof(c_0_142,plain,
! [X1977,X1978,X1979] :
( ( ~ class_Lattices_Obounded__lattice__bot(X1979)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1979),X1978),X1977) = c_Orderings_Obot__class_Obot(X1979)
| X1977 != c_Orderings_Obot__class_Obot(X1979)
| X1978 != c_Orderings_Obot__class_Obot(X1979) )
& ( ~ class_Lattices_Obounded__lattice__bot(X1979)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1979),X1978),X1977) != c_Orderings_Obot__class_Obot(X1979)
| X1977 = c_Orderings_Obot__class_Obot(X1979) )
& ( ~ class_Lattices_Obounded__lattice__bot(X1979)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1979),X1978),X1977) != c_Orderings_Obot__class_Obot(X1979)
| X1978 = c_Orderings_Obot__class_Obot(X1979) ) ),
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_143,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_135]) ).
cnf(c_0_144,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_136,c_0_114]),c_0_116])]) ).
fof(c_0_145,plain,
! [X2225] :
( ~ hBOOL(X2225)
| ~ hBOOL(hAPP(c_fNot,X2225)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_137])]) ).
cnf(c_0_146,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = X2 ),
inference(spm,[status(thm)],[c_0_138,c_0_101]) ).
cnf(c_0_147,plain,
( hBOOL(hAPP(c_fNot,X1))
| hBOOL(X1) ),
inference(split_conjunct,[status(thm)],[c_0_139]) ).
cnf(c_0_148,plain,
( ~ hBOOL(hAPP(X1,hAPP(hAPP(c_Product__Type_OPair(X2,X3),esk5_3(X3,X2,X1)),esk6_3(X3,X2,X1))))
| hBOOL(hAPP(X1,X4)) ),
inference(split_conjunct,[status(thm)],[c_0_140]) ).
cnf(c_0_149,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_141,c_0_110]),c_0_105])]) ).
fof(c_0_150,plain,
! [X10,X11,X9] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X11),X10) = c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool))
<=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(X9),X3),X11))
=> ! [X5] :
( hBOOL(hAPP(hAPP(c_member(X9),X5),X10))
=> X3 != X5 ) ) ),
inference(fof_simplification,[status(thm)],[fact_disjoint__iff__not__equal]) ).
fof(c_0_151,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_152,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_142]) ).
cnf(c_0_153,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_143,c_0_144]),c_0_105])]) ).
cnf(c_0_154,plain,
class_Lattices_Obounded__lattice__bot(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Obounded__lattice__bot]) ).
fof(c_0_155,plain,
! [X2081,X2082,X2083] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2082,X2083)),X2081) = c_Orderings_Obot__class_Obot(X2083)
| ~ class_Orderings_Obot(X2083) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_bot__apply])])]) ).
cnf(c_0_156,plain,
( ~ hBOOL(X1)
| ~ hBOOL(hAPP(c_fNot,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_145]) ).
cnf(c_0_157,plain,
( hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,X2) ),
inference(spm,[status(thm)],[c_0_146,c_0_147]) ).
cnf(c_0_158,plain,
( ~ hBOOL(X1)
| hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X1),X2)) ),
inference(spm,[status(thm)],[c_0_148,c_0_149]) ).
fof(c_0_159,plain,
! [X2050,X2051,X2052,X2053,X2054,X2055,X2056,X2057] :
( ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2057,tc_HOL_Obool)),X2056),X2055) = c_Orderings_Obot__class_Obot(tc_fun(X2057,tc_HOL_Obool))
| esk97_3(X2055,X2056,X2057) = esk98_3(X2055,X2056,X2057) )
& ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2057,tc_HOL_Obool)),X2056),X2055) = c_Orderings_Obot__class_Obot(tc_fun(X2057,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2057),esk98_3(X2055,X2056,X2057)),X2055)) )
& ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2057,tc_HOL_Obool)),X2056),X2055) = c_Orderings_Obot__class_Obot(tc_fun(X2057,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2057),esk97_3(X2055,X2056,X2057)),X2056)) )
& ( X2053 != X2054
| ~ hBOOL(hAPP(hAPP(c_member(X2052),X2054),X2050))
| ~ hBOOL(hAPP(hAPP(c_member(X2052),X2053),X2051))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2052,tc_HOL_Obool)),X2051),X2050) != c_Orderings_Obot__class_Obot(tc_fun(X2052,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_150])])])])])])]) ).
fof(c_0_160,plain,
! [X23,X9] : ~ hBOOL(hAPP(hAPP(c_member(X9),X23),c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)))),
inference(fof_simplification,[status(thm)],[fact_emptyE]) ).
cnf(c_0_161,plain,
( hAPP(X1,esk1_2(X2,X1)) != hAPP(X2,esk1_2(X2,X1))
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_151]) ).
cnf(c_0_162,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(er,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_152,c_0_153]),c_0_154])])]) ).
cnf(c_0_163,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_155]) ).
cnf(c_0_164,plain,
class_Orderings_Obot(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Obot]) ).
cnf(c_0_165,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,hAPP(c_fNot,X2)) ),
inference(spm,[status(thm)],[c_0_156,c_0_157]) ).
cnf(c_0_166,plain,
( ~ hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2))
| hBOOL(X1) ),
inference(spm,[status(thm)],[c_0_158,c_0_153]) ).
cnf(c_0_167,plain,
( hBOOL(hAPP(X1,esk100_2(X1,X2)))
| X1 = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_69,c_0_59]) ).
cnf(c_0_168,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]) ).
cnf(c_0_169,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_159]) ).
fof(c_0_170,plain,
! [X1966,X1967] : ~ hBOOL(hAPP(hAPP(c_member(X1967),X1966),c_Orderings_Obot__class_Obot(tc_fun(X1967,tc_HOL_Obool)))),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_160])]) ).
cnf(c_0_171,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_161,c_0_162]) ).
cnf(c_0_172,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_163,c_0_164]) ).
cnf(c_0_173,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_165,c_0_101]) ).
cnf(c_0_174,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_166,c_0_167]) ).
cnf(c_0_175,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)),
inference(spm,[status(thm)],[c_0_69,c_0_168]) ).
cnf(c_0_176,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_169]) ).
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____)),c_Arrow__Order__Mirabelle_OLin)),
inference(split_conjunct,[status(thm)],[fact__096F_AQ_A_058_ALin_096]) ).
fof(c_0_178,plain,
! [X570,X571] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X571,tc_HOL_Obool)),X570),X570) = X570,
inference(variable_rename,[status(thm)],[fact_Int__absorb]) ).
cnf(c_0_179,plain,
~ hBOOL(hAPP(hAPP(c_member(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)))),
inference(split_conjunct,[status(thm)],[c_0_170]) ).
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_171,c_0_172]) ).
cnf(c_0_181,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_156,c_0_173]),c_0_101])]) ).
cnf(c_0_182,plain,
( hBOOL(X1)
| c_Orderings_Obot__class_Obot(tc_HOL_Obool) = X1 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_174]),c_0_172]) ).
cnf(c_0_183,plain,
hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_146,c_0_175]) ).
fof(c_0_184,plain,
! [X1930,X1931,X1932,X1933] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1933,tc_HOL_Obool)),X1932),c_Set_Oinsert(X1933,X1931,X1930)) = c_Set_Oinsert(X1933,X1931,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1933,tc_HOL_Obool)),X1932),X1930)),
inference(variable_rename,[status(thm)],[fact_Un__insert__right]) ).
cnf(c_0_185,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_Q____),c_Arrow__Order__Mirabelle_OProf)),
inference(split_conjunct,[status(thm)],[fact__096Q_A_058_AProf_096]) ).
cnf(c_0_186,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_176,c_0_177]) ).
cnf(c_0_187,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_178]) ).
cnf(c_0_188,plain,
~ hBOOL(hAPP(hAPP(c_member(X1),X2),c_Orderings_Obot__class_Obot(tc_fun(v_F,tc_HOL_Obool)))),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_179,c_0_180]),c_0_180]) ).
cnf(c_0_189,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_181,c_0_182]),c_0_183]) ).
cnf(c_0_190,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_184]) ).
cnf(c_0_191,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_Q____),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_176,c_0_185]) ).
cnf(c_0_192,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_186,c_0_187]),c_0_177])]) ).
cnf(c_0_193,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_F,tc_HOL_Obool)) = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_188,c_0_62]) ).
cnf(c_0_194,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(spm,[status(thm)],[c_0_138,c_0_175]) ).
cnf(c_0_195,plain,
( hBOOL(X1)
| hAPP(c_fNot,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)) = X1 ),
inference(rw,[status(thm)],[c_0_182,c_0_189]) ).
cnf(c_0_196,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_63,c_0_190]) ).
cnf(c_0_197,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_191,c_0_187]),c_0_185])]) ).
cnf(c_0_198,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_F,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(rw,[status(thm)],[c_0_192,c_0_193]) ).
cnf(c_0_199,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_194,c_0_195]) ).
cnf(c_0_200,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_196,c_0_87]) ).
cnf(c_0_201,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_H____),v_b_H____)),hAPP(v_F,v_Q____))),
inference(split_conjunct,[status(thm)],[fact__096a_H_A_060_092_060_094bsub_062F_AQ_092_060_094esub_062_Ab_H_096]) ).
fof(c_0_202,plain,
! [X1975,X1976] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1976,tc_HOL_Obool)),c_Orderings_Obot__class_Obot(tc_fun(X1976,tc_HOL_Obool))),X1975) = X1975,
inference(variable_rename,[status(thm)],[fact_Un__empty__left]) ).
cnf(c_0_203,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_F,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OProf,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_197,c_0_180]),c_0_180]) ).
cnf(c_0_204,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(spm,[status(thm)],[c_0_198,c_0_193]) ).
cnf(c_0_205,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_199,c_0_199]) ).
cnf(c_0_206,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_200,c_0_201]) ).
cnf(c_0_207,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_202]) ).
cnf(c_0_208,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_203,c_0_193]) ).
cnf(c_0_209,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OLin
| 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_204,c_0_205])]) ).
fof(c_0_210,plain,
! [X348,X349,X350] :
( ( hBOOL(hAPP(hAPP(c_member(X350),X349),hAPP(c_fequal,X348)))
| X349 != X348 )
& ( X349 = X348
| ~ hBOOL(hAPP(hAPP(c_member(X350),X349),hAPP(c_fequal,X348))) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_eq__mem])])]) ).
cnf(c_0_211,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_206,c_0_207]) ).
cnf(c_0_212,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) != c_Arrow__Order__Mirabelle_OProf
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OLin ),
inference(spm,[status(thm)],[c_0_208,c_0_209]) ).
cnf(c_0_213,plain,
( X1 != X2
| hBOOL(hAPP(hAPP(c_member(X3),X1),hAPP(c_fequal,X2))) ),
inference(split_conjunct,[status(thm)],[c_0_210]) ).
cnf(c_0_214,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_F,tc_HOL_Obool)) != hAPP(v_F,v_Q____),
inference(rw,[status(thm)],[c_0_211,c_0_193]) ).
cnf(c_0_215,plain,
( c_Arrow__Order__Mirabelle_OProf = 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_212,c_0_205])]) ).
cnf(c_0_216,plain,
hBOOL(hAPP(hAPP(c_member(X1),X2),hAPP(c_fequal,X2))),
inference(er,[status(thm)],[c_0_213]) ).
cnf(c_0_217,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != hAPP(v_F,v_Q____),
inference(spm,[status(thm)],[c_0_214,c_0_193]) ).
cnf(c_0_218,plain,
( hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) != c_Arrow__Order__Mirabelle_OLin
| c_Arrow__Order__Mirabelle_OLin = c_Arrow__Order__Mirabelle_OProf ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_204,c_0_215]),c_0_208]) ).
fof(c_0_219,plain,
! [X22,X23,X13] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X13),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),X23),X22)),X13))
=> ~ 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),X22),X23)),X13)) ) ),
inference(fof_simplification,[status(thm)],[fact_Lin__irrefl]) ).
cnf(c_0_220,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_176,c_0_216]) ).
cnf(c_0_221,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_OLin ),
inference(spm,[status(thm)],[c_0_217,c_0_209]) ).
cnf(c_0_222,plain,
c_Arrow__Order__Mirabelle_OLin = c_Arrow__Order__Mirabelle_OProf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_218,c_0_215])]) ).
fof(c_0_223,plain,
! [X229,X230,X231] :
( ~ 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),X229),X230)),X231))
| ~ 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),X230),X229)),X231))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X231),c_Arrow__Order__Mirabelle_OLin)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_219])])]) ).
cnf(c_0_224,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_225,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_220,c_0_187]),c_0_216])]) ).
cnf(c_0_226,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____))),
inference(spm,[status(thm)],[c_0_69,c_0_177]) ).
cnf(c_0_227,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(rw,[status(thm)],[c_0_221,c_0_222]) ).
cnf(c_0_228,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_223]) ).
fof(c_0_229,plain,
! [X1558,X1559,X1560,X1561] : c_Fun_Ofun__upd(X1561,X1560,X1559,X1558,hAPP(X1559,X1558)) = X1559,
inference(variable_rename,[status(thm)],[fact_fun__upd__triv]) ).
cnf(c_0_230,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),
inference(spm,[status(thm)],[c_0_69,c_0_224]) ).
cnf(c_0_231,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_OLin ),
inference(spm,[status(thm)],[c_0_225,c_0_209]) ).
cnf(c_0_232,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)) = X1 ),
inference(spm,[status(thm)],[c_0_138,c_0_226]) ).
cnf(c_0_233,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_227,c_0_205])]) ).
cnf(c_0_234,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_228,c_0_216]) ).
cnf(c_0_235,plain,
c_Fun_Ofun__upd(X1,X2,X3,X4,hAPP(X3,X4)) = X3,
inference(split_conjunct,[status(thm)],[c_0_229]) ).
cnf(c_0_236,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_194,c_0_230]) ).
cnf(c_0_237,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(rw,[status(thm)],[c_0_231,c_0_222]) ).
cnf(c_0_238,plain,
( hBOOL(X2)
| X1 = X2
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(spm,[status(thm)],[c_0_175,c_0_205]) ).
cnf(c_0_239,plain,
hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_232,c_0_175]) ).
cnf(c_0_240,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_208,c_0_233]),c_0_217]) ).
cnf(c_0_241,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_234,c_0_216]) ).
cnf(c_0_242,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_235,c_0_236]) ).
cnf(c_0_243,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_237,c_0_238])]) ).
cnf(c_0_244,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_239,c_0_222]) ).
cnf(c_0_245,plain,
hAPP(v_F,v_Q____) = c_Arrow__Order__Mirabelle_OProf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_240,c_0_233])]) ).
cnf(c_0_246,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_241,c_0_67]) ).
cnf(c_0_247,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_242,c_0_243]),c_0_242]) ).
cnf(c_0_248,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_244,c_0_245]) ).
cnf(c_0_249,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_246,c_0_247]),c_0_222]),c_0_248]),c_0_175])]) ).
cnf(c_0_250,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_194,c_0_249]) ).
cnf(c_0_251,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_199,c_0_250]),c_0_250]) ).
cnf(c_0_252,plain,
hAPP(c_fequal,X1) != hAPP(c_fNot,c_Arrow__Order__Mirabelle_OProf),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_225,c_0_251]),c_0_208]) ).
cnf(c_0_253,plain,
hAPP(c_fequal,X1) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_252,c_0_251]) ).
cnf(c_0_254,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_246,c_0_253]),c_0_222]),c_0_248]),c_0_250]),c_0_249])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SCT134+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.45 % Computer : n016.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 04:38:53 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.53 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
% 25.16/4.31 % Version: 3.5.1
% 25.16/4.31 % Preprocessing class: FSLSSMSMSSSNFFN.
% 25.16/4.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 25.16/4.31 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 25.16/4.31 % Starting new_bool_3 with 300s (1) cores
% 25.16/4.31 % Starting new_bool_1 with 300s (1) cores
% 25.16/4.31 % Starting sh5l with 300s (1) cores
% 25.16/4.31 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 1563322 completed with status 0
% 25.16/4.31 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 25.16/4.31 % Preprocessing class: FSLSSMSMSSSNFFN.
% 25.16/4.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 25.16/4.31 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 25.16/4.31 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 25.16/4.31 % No SInE strategy applied
% 25.16/4.31 % Search class: FGHSM-FSLM33-DFFFFFNN
% 25.16/4.31 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 25.16/4.31 % Starting SubtermCWHack with 136s (1) cores
% 25.16/4.31 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 25.16/4.31 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 25.16/4.31 % Starting G-E--_302_C18_F1_URBAN_S5PRR_RG_S04BN with 136s (1) cores
% 25.16/4.31 % Starting G-E--_208_C09_12_F1_SE_CS_SP_PS_S070I with 136s (1) cores
% 25.16/4.31 % U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with pid 1563331 completed with status 0
% 25.16/4.31 % Result found by U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN
% 25.16/4.31 % Preprocessing class: FSLSSMSMSSSNFFN.
% 25.16/4.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 25.16/4.31 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 25.16/4.31 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 25.16/4.31 % No SInE strategy applied
% 25.16/4.31 % Search class: FGHSM-FSLM33-DFFFFFNN
% 25.16/4.31 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 25.16/4.31 % Starting SubtermCWHack with 136s (1) cores
% 25.16/4.31 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 25.16/4.31 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 25.16/4.31 % Preprocessing time : 0.013 s
% 25.16/4.31 % Presaturation interreduction done
% 25.16/4.31
% 25.16/4.31 % Proof found!
% 25.16/4.31 % SZS status ContradictoryAxioms
% 25.16/4.31 % SZS output start CNFRefutation
% See solution above
% 25.16/4.31 % Parsed axioms : 533
% 25.16/4.31 % Removed by relevancy pruning/SinE : 0
% 25.16/4.31 % Initial clauses : 807
% 25.16/4.31 % Removed in clause preprocessing : 38
% 25.16/4.31 % Initial clauses in saturation : 769
% 25.16/4.31 % Processed clauses : 9961
% 25.16/4.31 % ...of these trivial : 284
% 25.16/4.31 % ...subsumed : 6567
% 25.16/4.31 % ...remaining for further processing : 3110
% 25.16/4.31 % Other redundant clauses eliminated : 3059
% 25.16/4.31 % Clauses deleted for lack of memory : 0
% 25.16/4.31 % Backward-subsumed : 139
% 25.16/4.31 % Backward-rewritten : 659
% 25.16/4.31 % Generated clauses : 194791
% 25.16/4.31 % ...of the previous two non-redundant : 183182
% 25.16/4.31 % ...aggressively subsumed : 0
% 25.16/4.31 % Contextual simplify-reflections : 4
% 25.16/4.31 % Paramodulations : 191668
% 25.16/4.31 % Factorizations : 60
% 25.16/4.31 % NegExts : 0
% 25.16/4.31 % Equation resolutions : 3072
% 25.16/4.31 % Disequality decompositions : 0
% 25.16/4.31 % Total rewrite steps : 38013
% 25.16/4.31 % ...of those cached : 35557
% 25.16/4.31 % Propositional unsat checks : 0
% 25.16/4.31 % Propositional check models : 0
% 25.16/4.31 % Propositional check unsatisfiable : 0
% 25.16/4.31 % Propositional clauses : 0
% 25.16/4.31 % Propositional clauses after purity: 0
% 25.16/4.31 % Propositional unsat core size : 0
% 25.16/4.31 % Propositional preprocessing time : 0.000
% 25.16/4.31 % Propositional encoding time : 0.000
% 25.16/4.31 % Propositional solver time : 0.000
% 25.16/4.31 % Success case prop preproc time : 0.000
% 25.16/4.31 % Success case prop encoding time : 0.000
% 25.16/4.31 % Success case prop solver time : 0.000
% 25.16/4.31 % Current number of processed clauses : 1621
% 25.16/4.31 % Positive orientable unit clauses : 241
% 25.16/4.31 % Positive unorientable unit clauses: 14
% 25.16/4.31 % Negative unit clauses : 249
% 25.16/4.31 % Non-unit-clauses : 1117
% 25.16/4.31 % Current number of unprocessed clauses: 172386
% 25.16/4.31 % ...number of literals in the above : 594225
% 25.16/4.31 % Current number of archived formulas : 0
% 25.16/4.31 % Current number of archived clauses : 1427
% 25.16/4.31 % Clause-clause subsumption calls (NU) : 307595
% 25.16/4.31 % Rec. Clause-clause subsumption calls : 165658
% 25.16/4.31 % Non-unit clause-clause subsumptions : 3516
% 25.16/4.31 % Unit Clause-clause subsumption calls : 49875
% 25.16/4.31 % Rewrite failures with RHS unbound : 0
% 25.16/4.31 % BW rewrite match attempts : 5216
% 25.16/4.31 % BW rewrite match successes : 350
% 25.16/4.31 % Condensation attempts : 0
% 25.16/4.31 % Condensation successes : 0
% 25.16/4.31 % Termbank termtop insertions : 4071071
% 25.16/4.31 % Search garbage collected termcells : 12491
% 25.16/4.31
% 25.16/4.31 % -------------------------------------------------
% 25.16/4.31 % User time : 3.451 s
% 25.16/4.31 % System time : 0.148 s
% 25.16/4.31 % Total time : 3.599 s
% 25.16/4.31 % Maximum resident set size: 7780 pages
% 25.16/4.31
% 25.16/4.31 % -------------------------------------------------
% 25.16/4.31 % User time : 16.654 s
% 25.16/4.31 % System time : 0.691 s
% 25.16/4.31 % Total time : 17.345 s
% 25.16/4.31 % Maximum resident set size: 5376 pages
% 25.16/4.31 % E exiting
%------------------------------------------------------------------------------