%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SCT128+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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:07:55 PM UTC 2026
% Result : ContradictoryAxioms 25.21s 4.32s
% Output : CNFRefutation 25.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 54
% Syntax : Number of formulae : 303 ( 135 unt; 0 def)
% Number of atoms : 577 ( 229 equ)
% Maximal formula atoms : 10 ( 1 avg)
% Number of connectives : 509 ( 235 ~; 200 |; 22 &)
% ( 18 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-4 aty)
% Number of functors : 36 ( 36 usr; 11 con; 0-5 aty)
% Number of variables : 712 ( 124 sgn 337 !; 3 ?)
% 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_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(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_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(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,
! [X14,X15,X2,X9,X17] : hAPP(c_Fun_Ofun__upd(X17,X9,X2,X15,X14),X15) = X14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_fun__upd__same) ).
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(fact_emptyE,axiom,
! [X25,X9] : ~ hBOOL(hAPP(hAPP(c_member(X9),X25),c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_emptyE) ).
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(fact_accp_Osimps,axiom,
! [X25,X20,X9] :
( hBOOL(hAPP(c_Wellfounded_Oaccp(X9,X20),X25))
<=> ! [X3] :
( hBOOL(hAPP(hAPP(X20,X3),X25))
=> hBOOL(hAPP(c_Wellfounded_Oaccp(X9,X20),X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_accp_Osimps) ).
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_Int__commute,axiom,
! [X10,X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X11),X10) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X9,tc_HOL_Obool)),X10),X11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Int__commute) ).
fof(fact_le__infE,axiom,
! [X28,X29,X50,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X50,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X29),X28))
=> ~ ( c_Orderings_Oord__class_Oless__eq(X9,X50,X29)
=> ~ c_Orderings_Oord__class_Oless__eq(X9,X50,X28) ) ) ),
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(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(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(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_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(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__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(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_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_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_RangeP_Ointros,axiom,
! [X17,X9,X24,X25,X20] :
( hBOOL(hAPP(hAPP(X20,X25),X24))
=> c_Predicate_ORangeP(X9,X17,X20,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_RangeP_Ointros) ).
fof(fact_Lin__irrefl,axiom,
! [X24,X25,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),X25),X24)),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),X24),X25)),X13)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Lin__irrefl) ).
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_RangeP_Oequations,axiom,
! [X36,X20,X17,X9] :
( c_Predicate_ORangeP(X9,X17,X20,X36)
<=> ? [X6] : hBOOL(hAPP(hAPP(X20,X6),X36)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_RangeP_Oequations) ).
fof(fact_insertI1,axiom,
! [X10,X25,X9] : hBOOL(hAPP(hAPP(c_member(X9),X25),c_Set_Oinsert(X9,X25,X10))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insertI1) ).
fof(fact_irrefl__def,axiom,
! [X20,X9] :
( c_Relation_Oirrefl(X9,X20)
<=> ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X9,X9)),hAPP(hAPP(c_Product__Type_OPair(X9,X9),X3),X3)),X20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_irrefl__def) ).
fof(fact_xt1_I6_J,axiom,
! [X53,X50,X51,X9] :
( class_Orderings_Oorder(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X51,X50)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X53,X51)
=> c_Orderings_Oord__class_Oless__eq(X9,X53,X50) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_xt1_I6_J) ).
fof(fact_insert__code,axiom,
! [X15,X11,X14,X9] :
( hBOOL(hAPP(c_Set_Oinsert(X9,X14,X11),X15))
<=> ( hBOOL(hAPP(X11,X15))
| X14 = X15 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__code) ).
fof(fact_insert__absorb,axiom,
! [X11,X25,X9] :
( hBOOL(hAPP(hAPP(c_member(X9),X25),X11))
=> c_Set_Oinsert(X9,X25,X11) = X11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_insert__absorb) ).
fof(arity_HOL__Obool__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_HOL__Obool__Orderings_Oorder) ).
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(fact_insert__not__empty,axiom,
! [X11,X25,X9] : c_Set_Oinsert(X9,X25,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_Un__insert__right,axiom,
! [X10,X25,X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X11),c_Set_Oinsert(X9,X25,X10)) = c_Set_Oinsert(X9,X25,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_Un__Diff__cancel,axiom,
! [X10,X11,X9] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X9,tc_HOL_Obool)),X11),c_Groups_Ominus__class_Ominus(tc_fun(X9,tc_HOL_Obool),X10,X11)) = 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__Diff__cancel) ).
fof(help_c__fequal__1,axiom,
! [X14,X15] :
( X15 = X14
| ~ hBOOL(hAPP(hAPP(c_fequal,X15),X14)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_c__fequal__1) ).
fof(c_0_54,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_55,plain,
! [X2139,X2140,X2141,X2142] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X2142),X2141),c_Groups_Ominus__class_Ominus(tc_fun(X2142,tc_HOL_Obool),X2140,X2139)))
| ~ hBOOL(hAPP(hAPP(c_member(X2142),X2141),X2139)) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X2142),X2141),c_Groups_Ominus__class_Ominus(tc_fun(X2142,tc_HOL_Obool),X2140,X2139)))
| hBOOL(hAPP(hAPP(c_member(X2142),X2141),X2140)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_DiffE])])])]) ).
fof(c_0_56,plain,
! [X2074,X2075,X2077,X2078,X2079] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X2078),X2079),X2077))
| X2077 != c_Orderings_Obot__class_Obot(tc_fun(X2078,tc_HOL_Obool)) )
& ( X2074 = c_Orderings_Obot__class_Obot(tc_fun(X2075,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2075),esk100_2(X2074,X2075)),X2074)) ) ),
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_54])])])])])]) ).
cnf(c_0_57,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_55]) ).
cnf(c_0_58,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_56]) ).
fof(c_0_59,plain,
! [X164,X165,X166] :
( ( hBOOL(hAPP(hAPP(c_member(X166),X165),X164))
| ~ hBOOL(hAPP(X164,X165)) )
& ( hBOOL(hAPP(X164,X165))
| ~ hBOOL(hAPP(hAPP(c_member(X166),X165),X164)) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_mem__def])])]) ).
fof(c_0_60,plain,
! [X2151,X2152,X2153] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2153,tc_HOL_Obool)),c_Groups_Ominus__class_Ominus(tc_fun(X2153,tc_HOL_Obool),X2152,X2151)),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2153,tc_HOL_Obool)),X2152),X2151)) = X2152,
inference(variable_rename,[status(thm)],[fact_Un__Diff__Int]) ).
fof(c_0_61,plain,
! [X1767,X1768,X1769] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1769,tc_HOL_Obool)),X1768),X1767) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1769,tc_HOL_Obool)),X1767),X1768),
inference(variable_rename,[status(thm)],[fact_Un__commute]) ).
cnf(c_0_62,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_57,c_0_58]) ).
cnf(c_0_63,plain,
( ~ hBOOL(hAPP(X1,X2))
| hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
fof(c_0_64,plain,
! [X2216,X2217,X2218,X2219] : hAPP(c_COMBK(X2219,X2218,X2217),X2216) = X2217,
inference(variable_rename,[status(thm)],[help_c__COMBK__1]) ).
cnf(c_0_65,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_60]) ).
cnf(c_0_66,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_61]) ).
cnf(c_0_67,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_62,c_0_63]) ).
cnf(c_0_68,plain,
hAPP(c_COMBK(X1,X2,X3),X4) = X3,
inference(split_conjunct,[status(thm)],[c_0_64]) ).
fof(c_0_69,plain,
! [X1972,X1973] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1973,tc_HOL_Obool)),X1972),c_Orderings_Obot__class_Obot(tc_fun(X1973,tc_HOL_Obool))) = X1972,
inference(variable_rename,[status(thm)],[fact_Un__empty__right]) ).
fof(c_0_70,plain,
! [X1150,X1151,X1152] : c_Orderings_Oord__class_Oless__eq(tc_fun(X1152,tc_HOL_Obool),hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1152,tc_HOL_Obool)),X1151),X1150),X1150),
inference(variable_rename,[status(thm)],[fact_Int__lower2]) ).
cnf(c_0_71,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_65,c_0_66]) ).
cnf(c_0_72,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_67,c_0_68]) ).
cnf(c_0_73,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_69]) ).
fof(c_0_74,plain,
! [X1241,X1242,X1243,X1244,X1245] :
( ( ~ class_Orderings_Oord(X1244)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X1243,X1244),X1242,X1241)
| ~ c_Orderings_Oord__class_Oless__eq(X1244,hAPP(X1242,esk75_4(X1241,X1242,X1243,X1244)),hAPP(X1241,esk75_4(X1241,X1242,X1243,X1244))) )
& ( ~ class_Orderings_Oord(X1244)
| c_Orderings_Oord__class_Oless__eq(X1244,hAPP(X1242,X1245),hAPP(X1241,X1245))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X1243,X1244),X1242,X1241) ) ),
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_75,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_70]) ).
cnf(c_0_76,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_71,c_0_72]),c_0_73]) ).
cnf(c_0_77,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_74]) ).
cnf(c_0_78,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_75,c_0_76]) ).
cnf(c_0_79,plain,
class_Orderings_Oord(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Oord]) ).
fof(c_0_80,plain,
! [X1598,X1599,X1600,X1601,X1602] : hAPP(c_Fun_Ofun__upd(X1602,X1601,X1600,X1599,X1598),X1599) = X1598,
inference(variable_rename,[status(thm)],[fact_fun__upd__same]) ).
fof(c_0_81,plain,
! [X1101,X1102,X1103] :
( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1103),X1102),X1101) = X1102
| ~ c_Orderings_Oord__class_Oless__eq(X1103,X1102,X1101)
| ~ class_Lattices_Osemilattice__inf(X1103) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inf__absorb1])])]) ).
cnf(c_0_82,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_77,c_0_78]),c_0_68]),c_0_79])]) ).
cnf(c_0_83,plain,
hAPP(c_Fun_Ofun__upd(X1,X2,X3,X4,X5),X4) = X5,
inference(split_conjunct,[status(thm)],[c_0_80]) ).
fof(c_0_84,plain,
! [X25,X9] : ~ hBOOL(hAPP(hAPP(c_member(X9),X25),c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)))),
inference(fof_simplification,[status(thm)],[fact_emptyE]) ).
fof(c_0_85,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_86,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_81]) ).
cnf(c_0_87,plain,
( ~ hBOOL(X2)
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,X2) ),
inference(spm,[status(thm)],[c_0_82,c_0_83]) ).
cnf(c_0_88,plain,
class_Lattices_Osemilattice__inf(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Osemilattice__inf]) ).
fof(c_0_89,plain,
! [X1965,X1966] : ~ hBOOL(hAPP(hAPP(c_member(X1966),X1965),c_Orderings_Obot__class_Obot(tc_fun(X1966,tc_HOL_Obool)))),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_84])]) ).
fof(c_0_90,plain,
! [X374,X375,X376,X377,X378,X379,X380] :
( ( hBOOL(hAPP(c_Wellfounded_Oaccp(X380,X379),X378))
| ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X380,X379),esk27_3(X378,X379,X380))) )
& ( hBOOL(hAPP(c_Wellfounded_Oaccp(X380,X379),X378))
| hBOOL(hAPP(hAPP(X379,esk27_3(X378,X379,X380)),X378)) )
& ( hBOOL(hAPP(c_Wellfounded_Oaccp(X376,X375),X377))
| ~ hBOOL(hAPP(hAPP(X375,X377),X374))
| ~ hBOOL(hAPP(c_Wellfounded_Oaccp(X376,X375),X374)) ) ),
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)],[fact_accp_Osimps])])])])])])]) ).
cnf(c_0_91,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_85]) ).
cnf(c_0_92,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_86,c_0_87]),c_0_88])]) ).
cnf(c_0_93,plain,
class_Lattices_Olattice(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Olattice]) ).
cnf(c_0_94,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_89]) ).
cnf(c_0_95,plain,
( hBOOL(hAPP(c_Wellfounded_Oaccp(X3,X1),X2))
| hBOOL(hAPP(hAPP(X1,esk27_3(X2,X1,X3)),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
fof(c_0_96,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_97,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_91,c_0_92]),c_0_93])]) ).
cnf(c_0_98,plain,
hBOOL(hAPP(c_Wellfounded_Oaccp(X1,c_member(X2)),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)))),
inference(spm,[status(thm)],[c_0_94,c_0_95]) ).
fof(c_0_99,plain,
! [X544,X545,X546] : hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X546,tc_HOL_Obool)),X545),X544) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X546,tc_HOL_Obool)),X544),X545),
inference(variable_rename,[status(thm)],[fact_Int__commute]) ).
fof(c_0_100,plain,
! [X28,X29,X50,X9] :
( class_Lattices_Osemilattice__inf(X9)
=> ( c_Orderings_Oord__class_Oless__eq(X9,X50,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X9),X29),X28))
=> ~ ( c_Orderings_Oord__class_Oless__eq(X9,X50,X29)
=> ~ c_Orderings_Oord__class_Oless__eq(X9,X50,X28) ) ) ),
inference(fof_simplification,[status(thm)],[fact_le__infE]) ).
fof(c_0_101,plain,
! [X1116,X1117,X1118] :
( ( ~ class_Lattices_Osemilattice__inf(X1118)
| c_Orderings_Oord__class_Oless__eq(X1118,X1117,X1116)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1118),X1117),X1116) != X1117 )
& ( ~ class_Lattices_Osemilattice__inf(X1118)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1118),X1117),X1116) = X1117
| ~ c_Orderings_Oord__class_Oless__eq(X1118,X1117,X1116) ) ),
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_102,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_96]) ).
cnf(c_0_103,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X1) = X1,
inference(spm,[status(thm)],[c_0_97,c_0_98]) ).
cnf(c_0_104,plain,
hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X2),X3) = hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),X3),X2),
inference(split_conjunct,[status(thm)],[c_0_99]) ).
fof(c_0_105,plain,
! [X14,X15] :
( hBOOL(hAPP(hAPP(c_fequal,X15),X14))
| X15 != X14 ),
inference(fof_simplification,[status(thm)],[help_c__fequal__2]) ).
fof(c_0_106,plain,
! [X1081,X1082,X1083,X1084] :
( ( ~ class_Lattices_Osemilattice__inf(X1084)
| ~ c_Orderings_Oord__class_Oless__eq(X1084,X1083,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1084),X1082),X1081))
| c_Orderings_Oord__class_Oless__eq(X1084,X1083,X1081) )
& ( ~ class_Lattices_Osemilattice__inf(X1084)
| ~ c_Orderings_Oord__class_Oless__eq(X1084,X1083,hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(X1084),X1082),X1081))
| c_Orderings_Oord__class_Oless__eq(X1084,X1083,X1082) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_100])])])]) ).
cnf(c_0_107,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_101]) ).
cnf(c_0_108,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_102,c_0_103]),c_0_93])]) ).
cnf(c_0_109,plain,
( ~ hBOOL(X4)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X1,tc_HOL_Obool)),c_COMBK(X2,X3,X4)),X5) = X5 ),
inference(spm,[status(thm)],[c_0_104,c_0_76]) ).
fof(c_0_110,plain,
! [X2240,X2241] :
( hBOOL(hAPP(hAPP(c_fequal,X2241),X2240))
| X2241 != X2240 ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_105])]) ).
cnf(c_0_111,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_106]) ).
cnf(c_0_112,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_107,c_0_108]),c_0_88])]) ).
cnf(c_0_113,plain,
( ~ hBOOL(X6)
| ~ hBOOL(X3)
| c_COMBK(X1,X2,X3) = c_COMBK(X4,X5,X6) ),
inference(spm,[status(thm)],[c_0_76,c_0_109]) ).
cnf(c_0_114,plain,
( X1 != X2
| hBOOL(hAPP(hAPP(c_fequal,X1),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_110]) ).
fof(c_0_115,plain,
! [X19] :
( hBOOL(hAPP(c_fNot,X19))
| hBOOL(X19) ),
inference(fof_simplification,[status(thm)],[help_c__fNot__2]) ).
fof(c_0_116,plain,
! [X1873,X1874,X1875] :
( hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1875),X1873),X1874) = X1873
| ~ c_Orderings_Oord__class_Oless__eq(X1875,X1874,X1873)
| ~ class_Lattices_Osemilattice__sup(X1875) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_sup__absorb1])])]) ).
fof(c_0_117,plain,
! [X1855,X1856,X1857] :
( ( ~ class_Lattices_Osemilattice__sup(X1857)
| c_Orderings_Oord__class_Oless__eq(X1857,X1856,X1855)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1857),X1856),X1855) != X1855 )
& ( ~ class_Lattices_Osemilattice__sup(X1857)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1857),X1856),X1855) = X1855
| ~ c_Orderings_Oord__class_Oless__eq(X1857,X1856,X1855) ) ),
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_118,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_111,c_0_112]),c_0_88])]) ).
fof(c_0_119,plain,
! [X19] :
( ~ hBOOL(X19)
| ~ hBOOL(hAPP(c_fNot,X19)) ),
inference(fof_simplification,[status(thm)],[help_c__fNot__1]) ).
cnf(c_0_120,plain,
( ~ hBOOL(X2)
| ~ hBOOL(X1)
| X1 = X2 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_113]),c_0_68]) ).
cnf(c_0_121,plain,
hBOOL(hAPP(hAPP(c_fequal,X1),X1)),
inference(er,[status(thm)],[c_0_114]) ).
fof(c_0_122,plain,
! [X2243] :
( hBOOL(hAPP(c_fNot,X2243))
| hBOOL(X2243) ),
inference(variable_rename,[status(thm)],[c_0_115]) ).
fof(c_0_123,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_124,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_116]) ).
cnf(c_0_125,plain,
class_Lattices_Osemilattice__sup(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Osemilattice__sup]) ).
fof(c_0_126,plain,
! [X1976,X1977,X1978] :
( ( ~ class_Lattices_Obounded__lattice__bot(X1978)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1978),X1977),X1976) = c_Orderings_Obot__class_Obot(X1978)
| X1976 != c_Orderings_Obot__class_Obot(X1978)
| X1977 != c_Orderings_Obot__class_Obot(X1978) )
& ( ~ class_Lattices_Obounded__lattice__bot(X1978)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1978),X1977),X1976) != c_Orderings_Obot__class_Obot(X1978)
| X1976 = c_Orderings_Obot__class_Obot(X1978) )
& ( ~ class_Lattices_Obounded__lattice__bot(X1978)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(X1978),X1977),X1976) != c_Orderings_Obot__class_Obot(X1978)
| X1977 = c_Orderings_Obot__class_Obot(X1978) ) ),
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_127,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_117]) ).
cnf(c_0_128,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_118,c_0_91]),c_0_93])]) ).
fof(c_0_129,plain,
! [X2242] :
( ~ hBOOL(X2242)
| ~ hBOOL(hAPP(c_fNot,X2242)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_119])]) ).
cnf(c_0_130,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = X2 ),
inference(spm,[status(thm)],[c_0_120,c_0_121]) ).
cnf(c_0_131,plain,
( hBOOL(hAPP(c_fNot,X1))
| hBOOL(X1) ),
inference(split_conjunct,[status(thm)],[c_0_122]) ).
cnf(c_0_132,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_123]) ).
cnf(c_0_133,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_124,c_0_87]),c_0_125])]) ).
fof(c_0_134,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_135,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_136,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_126]) ).
cnf(c_0_137,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_127,c_0_128]),c_0_125])]) ).
cnf(c_0_138,plain,
class_Lattices_Obounded__lattice__bot(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Lattices_Obounded__lattice__bot]) ).
fof(c_0_139,plain,
! [X2080,X2081,X2082] :
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(X2081,X2082)),X2080) = c_Orderings_Obot__class_Obot(X2082)
| ~ class_Orderings_Obot(X2082) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_bot__apply])])]) ).
cnf(c_0_140,plain,
( ~ hBOOL(X1)
| ~ hBOOL(hAPP(c_fNot,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_129]) ).
cnf(c_0_141,plain,
( hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,X2) ),
inference(spm,[status(thm)],[c_0_130,c_0_131]) ).
cnf(c_0_142,plain,
( ~ hBOOL(X1)
| hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X1),X2)) ),
inference(spm,[status(thm)],[c_0_132,c_0_133]) ).
cnf(c_0_143,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| hBOOL(hAPP(X3,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
fof(c_0_144,plain,
! [X2049,X2050,X2051,X2052,X2053,X2054,X2055,X2056] :
( ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2056,tc_HOL_Obool)),X2055),X2054) = c_Orderings_Obot__class_Obot(tc_fun(X2056,tc_HOL_Obool))
| esk97_3(X2054,X2055,X2056) = esk98_3(X2054,X2055,X2056) )
& ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2056,tc_HOL_Obool)),X2055),X2054) = c_Orderings_Obot__class_Obot(tc_fun(X2056,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2056),esk98_3(X2054,X2055,X2056)),X2054)) )
& ( hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2056,tc_HOL_Obool)),X2055),X2054) = c_Orderings_Obot__class_Obot(tc_fun(X2056,tc_HOL_Obool))
| hBOOL(hAPP(hAPP(c_member(X2056),esk97_3(X2054,X2055,X2056)),X2055)) )
& ( X2052 != X2053
| ~ hBOOL(hAPP(hAPP(c_member(X2051),X2053),X2049))
| ~ hBOOL(hAPP(hAPP(c_member(X2051),X2052),X2050))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_fun(X2051,tc_HOL_Obool)),X2050),X2049) != c_Orderings_Obot__class_Obot(tc_fun(X2051,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_134])])])])])])]) ).
cnf(c_0_145,plain,
( hAPP(X1,esk1_2(X2,X1)) != hAPP(X2,esk1_2(X2,X1))
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_135]) ).
cnf(c_0_146,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_136,c_0_137]),c_0_138])])]) ).
cnf(c_0_147,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_139]) ).
cnf(c_0_148,plain,
class_Orderings_Obot(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Obot]) ).
cnf(c_0_149,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_150,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_151,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_fNot,hAPP(c_fNot,X2)) ),
inference(spm,[status(thm)],[c_0_140,c_0_141]) ).
cnf(c_0_152,plain,
( ~ hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2))
| hBOOL(X1) ),
inference(spm,[status(thm)],[c_0_142,c_0_137]) ).
cnf(c_0_153,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_143,c_0_58]) ).
cnf(c_0_154,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_155,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_144]) ).
cnf(c_0_156,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_145,c_0_146]) ).
cnf(c_0_157,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_147,c_0_148]) ).
fof(c_0_158,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]) ).
cnf(c_0_159,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____))),
inference(spm,[status(thm)],[c_0_143,c_0_149]) ).
cnf(c_0_160,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),
inference(spm,[status(thm)],[c_0_143,c_0_150]) ).
cnf(c_0_161,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_151,c_0_121]) ).
cnf(c_0_162,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_152,c_0_153]) ).
cnf(c_0_163,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)),
inference(spm,[status(thm)],[c_0_143,c_0_154]) ).
cnf(c_0_164,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_155]) ).
fof(c_0_165,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_166,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_156,c_0_157]) ).
fof(c_0_167,plain,
! [X2068,X2069,X2070,X2071,X2072] :
( ( hBOOL(hAPP(hAPP(c_member(X2072),esk99_2(X2071,X2072)),X2071))
| X2071 = c_Orderings_Obot__class_Obot(tc_fun(X2072,tc_HOL_Obool)) )
& ( X2068 != c_Orderings_Obot__class_Obot(tc_fun(X2069,tc_HOL_Obool))
| ~ hBOOL(hAPP(hAPP(c_member(X2069),X2070),X2068)) ) ),
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_158])])])])])]) ).
cnf(c_0_168,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)) = X1 ),
inference(spm,[status(thm)],[c_0_120,c_0_159]) ).
cnf(c_0_169,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____) = X1 ),
inference(spm,[status(thm)],[c_0_120,c_0_160]) ).
cnf(c_0_170,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_140,c_0_161]),c_0_121])]) ).
cnf(c_0_171,plain,
( hBOOL(X1)
| c_Orderings_Obot__class_Obot(tc_HOL_Obool) = X1 ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103,c_0_162]),c_0_157]) ).
cnf(c_0_172,plain,
hAPP(hAPP(c_fequal,X1),X1) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_130,c_0_163]) ).
cnf(c_0_173,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_164,c_0_149]) ).
cnf(c_0_174,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_165]) ).
cnf(c_0_175,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_94,c_0_166]),c_0_166]) ).
cnf(c_0_176,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_167]) ).
cnf(c_0_177,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_168,c_0_160]) ).
cnf(c_0_178,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(spm,[status(thm)],[c_0_169,c_0_163]) ).
cnf(c_0_179,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_170,c_0_171]),c_0_172]) ).
cnf(c_0_180,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_164,c_0_150]) ).
cnf(c_0_181,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_173,c_0_174]),c_0_149])]) ).
cnf(c_0_182,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_175,c_0_176]) ).
cnf(c_0_183,plain,
( ~ hBOOL(X1)
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_168,c_0_177]),c_0_178]) ).
cnf(c_0_184,plain,
( hBOOL(X1)
| hAPP(c_fNot,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)) = X1 ),
inference(rw,[status(thm)],[c_0_171,c_0_179]) ).
cnf(c_0_185,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_180,c_0_174]),c_0_150])]) ).
cnf(c_0_186,plain,
c_Orderings_Obot__class_Obot(tc_fun(v_F,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(rw,[status(thm)],[c_0_181,c_0_182]) ).
cnf(c_0_187,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_183,c_0_184]) ).
fof(c_0_188,plain,
! [X903,X904,X905,X906,X907] :
( c_Predicate_ORangeP(X904,X903,X907,X905)
| ~ hBOOL(hAPP(hAPP(X907,X906),X905)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_RangeP_Ointros])])]) ).
fof(c_0_189,plain,
! [X24,X25,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),X25),X24)),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),X24),X25)),X13)) ) ),
inference(fof_simplification,[status(thm)],[fact_Lin__irrefl]) ).
fof(c_0_190,plain,
! [X310,X311,X312] :
( ( hBOOL(hAPP(hAPP(c_member(X312),X311),hAPP(c_fequal,X310)))
| X311 != X310 )
& ( X311 = X310
| ~ hBOOL(hAPP(hAPP(c_member(X312),X311),hAPP(c_fequal,X310))) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_eq__mem])])]) ).
cnf(c_0_191,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_185,c_0_166]),c_0_166]) ).
cnf(c_0_192,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OLin,
inference(spm,[status(thm)],[c_0_186,c_0_182]) ).
cnf(c_0_193,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_187,c_0_187]) ).
fof(c_0_194,plain,
! [X908,X909,X910,X911,X913,X914,X915,X916,X917] :
( ( c_Predicate_ORangeP(X917,X916,X914,X913)
| ~ hBOOL(hAPP(hAPP(X914,X915),X913)) )
& ( hBOOL(hAPP(hAPP(X909,esk71_2(X908,X909)),X908))
| ~ c_Predicate_ORangeP(X911,X910,X909,X908) ) ),
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_RangeP_Oequations])])])])])]) ).
cnf(c_0_195,plain,
( ~ hBOOL(hAPP(hAPP(X1,X2),X3))
| c_Predicate_ORangeP(X4,X5,X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_188]) ).
fof(c_0_196,plain,
! [X146,X147,X148] :
( ~ 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),X146),X147)),X148))
| ~ 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),X147),X146)),X148))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X148),c_Arrow__Order__Mirabelle_OLin)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_189])])]) ).
fof(c_0_197,plain,
! [X1430,X1431,X1432] : hBOOL(hAPP(hAPP(c_member(X1432),X1431),c_Set_Oinsert(X1432,X1431,X1430))),
inference(variable_rename,[status(thm)],[fact_insertI1]) ).
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_190]) ).
cnf(c_0_199,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_191,c_0_182]) ).
cnf(c_0_200,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_192,c_0_193])]) ).
cnf(c_0_201,plain,
( ~ c_Predicate_ORangeP(X1,X2,X3,X4)
| hBOOL(hAPP(hAPP(X3,esk71_2(X4,X3)),X4)) ),
inference(split_conjunct,[status(thm)],[c_0_194]) ).
cnf(c_0_202,plain,
( ~ hBOOL(X3)
| c_Predicate_ORangeP(X1,X2,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X3) ),
inference(spm,[status(thm)],[c_0_195,c_0_103]) ).
cnf(c_0_203,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_196]) ).
cnf(c_0_204,plain,
hBOOL(hAPP(hAPP(c_member(X1),X2),c_Set_Oinsert(X1,X2,X3))),
inference(split_conjunct,[status(thm)],[c_0_197]) ).
cnf(c_0_205,plain,
hBOOL(hAPP(hAPP(c_member(X1),X2),hAPP(c_fequal,X2))),
inference(er,[status(thm)],[c_0_198]) ).
cnf(c_0_206,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_199,c_0_200]) ).
cnf(c_0_207,plain,
( ~ hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2))
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),X1),X2) = X2 ),
inference(spm,[status(thm)],[c_0_92,c_0_108]) ).
cnf(c_0_208,plain,
( ~ hBOOL(X1)
| hBOOL(hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool))),X1)) ),
inference(spm,[status(thm)],[c_0_201,c_0_202]) ).
fof(c_0_209,plain,
! [X20,X9] :
( c_Relation_Oirrefl(X9,X20)
<=> ! [X3] : ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X9,X9)),hAPP(hAPP(c_Product__Type_OPair(X9,X9),X3),X3)),X20)) ),
inference(fof_simplification,[status(thm)],[fact_irrefl__def]) ).
cnf(c_0_210,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Set_Oinsert(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),X1),X3)),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)),c_Set_Oinsert(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),X1),X3))) ),
inference(spm,[status(thm)],[c_0_203,c_0_204]) ).
cnf(c_0_211,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_164,c_0_205]) ).
cnf(c_0_212,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_206,c_0_193])]) ).
fof(c_0_213,plain,
! [X1278,X1279,X1280,X1281] :
( c_Orderings_Oord__class_Oless__eq(X1281,X1278,X1279)
| ~ c_Orderings_Oord__class_Oless__eq(X1281,X1278,X1280)
| ~ c_Orderings_Oord__class_Oless__eq(X1281,X1280,X1279)
| ~ class_Orderings_Oorder(X1281) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_xt1_I6_J])])]) ).
cnf(c_0_214,plain,
( ~ hBOOL(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool),esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool))),X1) = X1 ),
inference(spm,[status(thm)],[c_0_207,c_0_208]) ).
cnf(c_0_215,plain,
( ~ hBOOL(X1)
| hBOOL(esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool))) ),
inference(spm,[status(thm)],[c_0_208,c_0_92]) ).
fof(c_0_216,plain,
! [X825,X826,X827,X828,X829] :
( ( c_Relation_Oirrefl(X829,X828)
| hBOOL(hAPP(hAPP(c_member(tc_prod(X829,X829)),hAPP(hAPP(c_Product__Type_OPair(X829,X829),esk58_2(X828,X829)),esk58_2(X828,X829))),X828)) )
& ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X826,X826)),hAPP(hAPP(c_Product__Type_OPair(X826,X826),X827),X827)),X825))
| ~ c_Relation_Oirrefl(X826,X825) ) ),
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_209])])])])])]) ).
fof(c_0_217,plain,
! [X1406,X1407,X1408,X1409] :
( ( hBOOL(hAPP(c_Set_Oinsert(X1409,X1408,X1407),X1406))
| ~ hBOOL(hAPP(X1407,X1406)) )
& ( hBOOL(hAPP(c_Set_Oinsert(X1409,X1408,X1407),X1406))
| X1408 != X1406 )
& ( hBOOL(hAPP(X1407,X1406))
| X1408 = X1406
| ~ hBOOL(hAPP(c_Set_Oinsert(X1409,X1408,X1407),X1406)) ) ),
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_218,plain,
~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Set_Oinsert(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),X1),X2)),c_Arrow__Order__Mirabelle_OLin)),
inference(spm,[status(thm)],[c_0_210,c_0_204]) ).
fof(c_0_219,plain,
! [X1415,X1416,X1417] :
( c_Set_Oinsert(X1417,X1416,X1415) = X1415
| ~ hBOOL(hAPP(hAPP(c_member(X1417),X1416),X1415)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_insert__absorb])])]) ).
cnf(c_0_220,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_211,c_0_174]),c_0_205])]) ).
cnf(c_0_221,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_192,c_0_212]),c_0_199]) ).
cnf(c_0_222,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X1,X4,X2)
| ~ c_Orderings_Oord__class_Oless__eq(X1,X2,X3)
| ~ class_Orderings_Oorder(X1)
| c_Orderings_Oord__class_Oless__eq(X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[c_0_213]) ).
cnf(c_0_223,plain,
class_Orderings_Oorder(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Oorder]) ).
cnf(c_0_224,plain,
( ~ hBOOL(X1)
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool))) ),
inference(spm,[status(thm)],[c_0_118,c_0_214]) ).
cnf(c_0_225,plain,
( ~ hBOOL(X2)
| hAPP(hAPP(c_fequal,X1),X1) = esk71_2(X2,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_130,c_0_215]) ).
cnf(c_0_226,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(X1,X1)),hAPP(hAPP(c_Product__Type_OPair(X1,X1),X3),X3)),X2))
| ~ c_Relation_Oirrefl(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_216]) ).
cnf(c_0_227,plain,
( X1 != X2
| hBOOL(hAPP(c_Set_Oinsert(X3,X1,X4),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_217]) ).
cnf(c_0_228,plain,
~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Set_Oinsert(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),X1),X2))),
inference(spm,[status(thm)],[c_0_218,c_0_63]) ).
cnf(c_0_229,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| c_Set_Oinsert(X1,X2,X3) = X3 ),
inference(split_conjunct,[status(thm)],[c_0_219]) ).
fof(c_0_230,plain,
! [X1557,X1558,X1559,X1560] : c_Fun_Ofun__upd(X1560,X1559,X1558,X1557,hAPP(X1558,X1557)) = X1558,
inference(variable_rename,[status(thm)],[fact_fun__upd__triv]) ).
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_220,c_0_200]) ).
cnf(c_0_232,plain,
c_Arrow__Order__Mirabelle_OLin = c_Arrow__Order__Mirabelle_OProf,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_221,c_0_212])]) ).
cnf(c_0_233,plain,
( ~ hBOOL(X3)
| ~ c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X3,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_222,c_0_87]),c_0_223])]) ).
cnf(c_0_234,plain,
( ~ hBOOL(X1)
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,hAPP(hAPP(c_fequal,X2),X2)) ),
inference(spm,[status(thm)],[c_0_224,c_0_225]) ).
cnf(c_0_235,plain,
hAPP(hAPP(c_fequal,X1),X1) = hAPP(hAPP(c_member(X2),X3),hAPP(c_fequal,X3)),
inference(spm,[status(thm)],[c_0_130,c_0_205]) ).
cnf(c_0_236,plain,
( ~ hBOOL(hAPP(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X1),X3),X3)))
| ~ c_Relation_Oirrefl(X1,X2) ),
inference(spm,[status(thm)],[c_0_226,c_0_63]) ).
cnf(c_0_237,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X2)),
inference(er,[status(thm)],[c_0_227]) ).
cnf(c_0_238,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X2))
| ~ 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),X1)),X2)) ),
inference(spm,[status(thm)],[c_0_228,c_0_229]) ).
cnf(c_0_239,plain,
( c_Relation_Oirrefl(X1,X2)
| hBOOL(hAPP(hAPP(c_member(tc_prod(X1,X1)),hAPP(hAPP(c_Product__Type_OPair(X1,X1),esk58_2(X2,X1)),esk58_2(X2,X1))),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_216]) ).
cnf(c_0_240,plain,
hAPP(hAPP(c_fequal,X1),X1) = hAPP(hAPP(c_fequal,X2),X2),
inference(spm,[status(thm)],[c_0_130,c_0_121]) ).
cnf(c_0_241,plain,
c_Fun_Ofun__upd(X1,X2,X3,X4,hAPP(X3,X4)) = X3,
inference(split_conjunct,[status(thm)],[c_0_230]) ).
cnf(c_0_242,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_232]) ).
cnf(c_0_243,plain,
( hBOOL(X2)
| X1 = X2
| hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = X1 ),
inference(spm,[status(thm)],[c_0_163,c_0_193]) ).
fof(c_0_244,plain,
! [X11,X25,X9] : c_Set_Oinsert(X9,X25,X11) != c_Orderings_Obot__class_Obot(tc_fun(X9,tc_HOL_Obool)),
inference(fof_simplification,[status(thm)],[fact_insert__not__empty]) ).
cnf(c_0_245,plain,
( ~ hBOOL(X3)
| c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,hAPP(hAPP(c_fequal,X2),X2)) ),
inference(spm,[status(thm)],[c_0_233,c_0_234]) ).
cnf(c_0_246,plain,
c_Predicate_ORangeP(X1,X2,c_member(X3),hAPP(c_fequal,X4)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_235]),c_0_121])]) ).
cnf(c_0_247,plain,
~ c_Relation_Oirrefl(X1,c_Set_Oinsert(X2,hAPP(hAPP(c_Product__Type_OPair(X1,X1),X3),X3),X4)),
inference(spm,[status(thm)],[c_0_236,c_0_237]) ).
cnf(c_0_248,plain,
( ~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,X1))
| c_Relation_Oirrefl(tc_Arrow__Order__Mirabelle_Oalt,X1) ),
inference(spm,[status(thm)],[c_0_238,c_0_239]) ).
cnf(c_0_249,plain,
c_Predicate_ORangeP(X1,X2,c_fequal,X3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_240]),c_0_121])]) ).
cnf(c_0_250,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_241,c_0_178]) ).
cnf(c_0_251,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_242,c_0_243])]) ).
fof(c_0_252,plain,
! [X1992,X1993,X1994] : c_Set_Oinsert(X1994,X1993,X1992) != c_Orderings_Obot__class_Obot(tc_fun(X1994,tc_HOL_Obool)),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_244])]) ).
fof(c_0_253,plain,
! [X1929,X1930,X1931,X1932] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1932,tc_HOL_Obool)),X1931),c_Set_Oinsert(X1932,X1930,X1929)) = c_Set_Oinsert(X1932,X1930,hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1932,tc_HOL_Obool)),X1931),X1929)),
inference(variable_rename,[status(thm)],[fact_Un__insert__right]) ).
fof(c_0_254,plain,
! [X2161,X2162,X2163] : hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2163,tc_HOL_Obool)),X2162),c_Groups_Ominus__class_Ominus(tc_fun(X2163,tc_HOL_Obool),X2161,X2162)) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X2163,tc_HOL_Obool)),X2162),X2161),
inference(variable_rename,[status(thm)],[fact_Un__Diff__cancel]) ).
cnf(c_0_255,plain,
c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X1,hAPP(hAPP(c_fequal,X2),X2)),
inference(spm,[status(thm)],[c_0_245,c_0_98]) ).
cnf(c_0_256,plain,
( ~ hBOOL(hAPP(hAPP(c_member(X1),X2),hAPP(c_fequal,X3)))
| X2 = X3 ),
inference(split_conjunct,[status(thm)],[c_0_190]) ).
cnf(c_0_257,plain,
hBOOL(hAPP(hAPP(c_member(X1),esk71_2(hAPP(c_fequal,X2),c_member(X1))),hAPP(c_fequal,X2))),
inference(spm,[status(thm)],[c_0_201,c_0_246]) ).
cnf(c_0_258,plain,
~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OLin,c_Set_Oinsert(X1,hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X2),X3))),
inference(spm,[status(thm)],[c_0_247,c_0_248]) ).
cnf(c_0_259,plain,
hBOOL(hAPP(hAPP(c_fequal,esk71_2(X1,c_fequal)),X1)),
inference(spm,[status(thm)],[c_0_201,c_0_249]) ).
cnf(c_0_260,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_250,c_0_251]),c_0_250]) ).
cnf(c_0_261,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_252]) ).
cnf(c_0_262,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_253]) ).
cnf(c_0_263,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),c_Groups_Ominus__class_Ominus(tc_fun(X1,tc_HOL_Obool),X3,X2)) = hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),X2),X3),
inference(split_conjunct,[status(thm)],[c_0_254]) ).
cnf(c_0_264,plain,
( ~ hBOOL(X1)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool))),X1) = esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_224]),c_0_125])]) ).
cnf(c_0_265,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X1),hAPP(hAPP(c_fequal,X2),X2)) = hAPP(hAPP(c_fequal,X2),X2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_127,c_0_255]),c_0_125])]) ).
cnf(c_0_266,plain,
esk71_2(hAPP(c_fequal,X1),c_member(X2)) = X1,
inference(spm,[status(thm)],[c_0_256,c_0_257]) ).
cnf(c_0_267,plain,
~ hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,c_Set_Oinsert(X1,hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X2),X3))),
inference(spm,[status(thm)],[c_0_258,c_0_232]) ).
cnf(c_0_268,plain,
( hBOOL(c_Arrow__Order__Mirabelle_OProf)
| hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,X1)) ),
inference(spm,[status(thm)],[c_0_259,c_0_260]) ).
cnf(c_0_269,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_261,c_0_262]) ).
cnf(c_0_270,plain,
( ~ hBOOL(X4)
| hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_fun(X1,tc_HOL_Obool)),c_COMBK(X2,X3,X4)),X5) = c_COMBK(X2,X3,X4) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_263,c_0_72]),c_0_73]) ).
cnf(c_0_271,plain,
( hAPP(X1,esk1_2(c_COMBK(X2,X3,X4),X1)) != X4
| X1 = c_COMBK(X2,X3,X4) ),
inference(spm,[status(thm)],[c_0_145,c_0_68]) ).
cnf(c_0_272,plain,
hAPP(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),hAPP(hAPP(c_fequal,X1),X1)),X2) = hAPP(hAPP(c_fequal,X1),X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_255]),c_0_125])]) ).
cnf(c_0_273,plain,
esk71_2(hAPP(hAPP(c_fequal,X1),X1),c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)) = hAPP(hAPP(c_fequal,X1),X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_264,c_0_265]),c_0_121])]) ).
cnf(c_0_274,plain,
hAPP(hAPP(c_fequal,v_F),v_F) = hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_168,c_0_257]),c_0_266]),c_0_235]) ).
cnf(c_0_275,plain,
hBOOL(c_Arrow__Order__Mirabelle_OProf),
inference(spm,[status(thm)],[c_0_267,c_0_268]) ).
cnf(c_0_276,plain,
( ~ hBOOL(X3)
| c_COMBK(X1,X2,X3) != c_Orderings_Obot__class_Obot(tc_fun(X4,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_269,c_0_270]) ).
cnf(c_0_277,plain,
c_COMBK(X1,X2,hAPP(hAPP(c_fequal,X3),X3)) = hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),hAPP(hAPP(c_fequal,X3),X3)),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_271,c_0_272])]) ).
cnf(c_0_278,plain,
esk71_2(hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)),c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)) = hAPP(c_Arrow__Order__Mirabelle_OLin,hAPP(v_F,v_Q____)),
inference(spm,[status(thm)],[c_0_273,c_0_274]) ).
cnf(c_0_279,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_183,c_0_275]) ).
cnf(c_0_280,plain,
hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),hAPP(hAPP(c_fequal,X1),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_276,c_0_277]),c_0_121])]) ).
cnf(c_0_281,plain,
esk71_2(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_278,c_0_177]),c_0_177]) ).
cnf(c_0_282,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_187,c_0_279]),c_0_279]) ).
cnf(c_0_283,plain,
( ~ hBOOL(X1)
| hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),esk71_2(X1,c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool))) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_280,c_0_225]) ).
cnf(c_0_284,plain,
esk71_2(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),c_Lattices_Osemilattice__inf__class_Oinf(tc_HOL_Obool)) = hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_281,c_0_178]),c_0_178]) ).
cnf(c_0_285,plain,
hAPP(c_fequal,X1) != hAPP(c_fNot,c_Arrow__Order__Mirabelle_OProf),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_220,c_0_282]),c_0_199]) ).
cnf(c_0_286,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),hAPP(c_Arrow__Order__Mirabelle_OProf,v_P_H____)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_283,c_0_284]),c_0_163])]) ).
cnf(c_0_287,plain,
( ~ hBOOL(X2)
| hAPP(X1,esk1_2(hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X2),X1)) != X2
| X1 = hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),X2) ),
inference(spm,[status(thm)],[c_0_145,c_0_133]) ).
cnf(c_0_288,plain,
hAPP(c_fequal,X1) = c_Arrow__Order__Mirabelle_OProf,
inference(spm,[status(thm)],[c_0_285,c_0_282]) ).
cnf(c_0_289,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf),
inference(rw,[status(thm)],[c_0_286,c_0_279]) ).
cnf(c_0_290,plain,
hAPP(c_Lattices_Osemilattice__sup__class_Osup(tc_HOL_Obool),c_Arrow__Order__Mirabelle_OProf) = c_fequal,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_287,c_0_288])]),c_0_275])]) ).
cnf(c_0_291,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_HOL_Obool)) != c_fequal,
inference(rw,[status(thm)],[c_0_289,c_0_290]) ).
fof(c_0_292,plain,
! [X14,X15] :
( X15 = X14
| ~ hBOOL(hAPP(hAPP(c_fequal,X15),X14)) ),
inference(fof_simplification,[status(thm)],[help_c__fequal__1]) ).
cnf(c_0_293,plain,
hAPP(c_fNot,c_Arrow__Order__Mirabelle_OProf) != c_fequal,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_282]),c_0_199]) ).
fof(c_0_294,plain,
! [X2238,X2239] :
( X2239 = X2238
| ~ hBOOL(hAPP(hAPP(c_fequal,X2239),X2238)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_292])]) ).
cnf(c_0_295,plain,
hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____) = c_Arrow__Order__Mirabelle_OProf,
inference(rw,[status(thm)],[c_0_178,c_0_279]) ).
cnf(c_0_296,plain,
c_Arrow__Order__Mirabelle_OProf = c_fequal,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_293,c_0_282])]) ).
cnf(c_0_297,plain,
( ~ hBOOL(hAPP(hAPP(c_fequal,X1),X2))
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_294]) ).
cnf(c_0_298,plain,
hAPP(c_fequal,v_P____) = c_fequal,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_295,c_0_296]),c_0_296]) ).
cnf(c_0_299,plain,
hBOOL(c_fequal),
inference(rw,[status(thm)],[c_0_275,c_0_296]) ).
cnf(c_0_300,plain,
hAPP(c_fNot,c_fequal) != c_fequal,
inference(rw,[status(thm)],[c_0_293,c_0_296]) ).
cnf(c_0_301,plain,
v_P____ = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_297,c_0_298]),c_0_288]),c_0_296]),c_0_299])]) ).
cnf(c_0_302,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_300,c_0_301]),c_0_301]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SCT128+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.02 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 04:33:21 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.03/0.34 Running first-order theorem proving
% 0.03/0.34 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.21/4.32 % Version: 3.5.1
% 25.21/4.32 % Preprocessing class: FSLSSMSMSSSNFFN.
% 25.21/4.32 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 25.21/4.32 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 25.21/4.32 % Starting new_bool_3 with 300s (1) cores
% 25.21/4.32 % Starting new_bool_1 with 300s (1) cores
% 25.21/4.32 % Starting sh5l with 300s (1) cores
% 25.21/4.32 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 1562178 completed with status 0
% 25.21/4.32 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 25.21/4.32 % Preprocessing class: FSLSSMSMSSSNFFN.
% 25.21/4.32 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 25.21/4.32 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 25.21/4.32 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 25.21/4.32 % No SInE strategy applied
% 25.21/4.32 % Search class: FGHSM-FSLM33-DFFFFFNN
% 25.21/4.32 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 25.21/4.32 % Starting SubtermCWHack with 136s (1) cores
% 25.21/4.32 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 25.21/4.32 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 25.21/4.32 % Starting G-E--_302_C18_F1_URBAN_S5PRR_RG_S04BN with 136s (1) cores
% 25.21/4.32 % Starting G-E--_208_C09_12_F1_SE_CS_SP_PS_S070I with 136s (1) cores
% 25.21/4.32 % U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with pid 1562187 completed with status 0
% 25.21/4.32 % Result found by U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN
% 25.21/4.32 % Preprocessing class: FSLSSMSMSSSNFFN.
% 25.21/4.32 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 25.21/4.32 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 25.21/4.32 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 25.21/4.32 % No SInE strategy applied
% 25.21/4.32 % Search class: FGHSM-FSLM33-DFFFFFNN
% 25.21/4.32 % Scheduled 11 strats onto 5 cores with 1500 seconds (1500 total)
% 25.21/4.32 % Starting SubtermCWHack with 136s (1) cores
% 25.21/4.32 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 25.21/4.32 % Starting U----_206b_01_C11_23_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 25.21/4.32 % Preprocessing time : 0.014 s
% 25.21/4.32 % Presaturation interreduction done
% 25.21/4.32
% 25.21/4.32 % Proof found!
% 25.21/4.32 % SZS status ContradictoryAxioms
% 25.21/4.32 % SZS output start CNFRefutation
% See solution above
% 25.21/4.33 % Parsed axioms : 533
% 25.21/4.33 % Removed by relevancy pruning/SinE : 0
% 25.21/4.33 % Initial clauses : 807
% 25.21/4.33 % Removed in clause preprocessing : 38
% 25.21/4.33 % Initial clauses in saturation : 769
% 25.21/4.33 % Processed clauses : 10325
% 25.21/4.33 % ...of these trivial : 268
% 25.21/4.33 % ...subsumed : 7038
% 25.21/4.33 % ...remaining for further processing : 3019
% 25.21/4.33 % Other redundant clauses eliminated : 3130
% 25.21/4.33 % Clauses deleted for lack of memory : 0
% 25.21/4.33 % Backward-subsumed : 144
% 25.21/4.33 % Backward-rewritten : 2167
% 25.21/4.33 % Generated clauses : 181985
% 25.21/4.33 % ...of the previous two non-redundant : 170548
% 25.21/4.33 % ...aggressively subsumed : 0
% 25.21/4.33 % Contextual simplify-reflections : 5
% 25.21/4.33 % Paramodulations : 178799
% 25.21/4.33 % Factorizations : 51
% 25.21/4.33 % NegExts : 0
% 25.21/4.33 % Equation resolutions : 3144
% 25.21/4.33 % Disequality decompositions : 0
% 25.21/4.33 % Total rewrite steps : 36526
% 25.21/4.33 % ...of those cached : 32061
% 25.21/4.33 % Propositional unsat checks : 0
% 25.21/4.33 % Propositional check models : 0
% 25.21/4.33 % Propositional check unsatisfiable : 0
% 25.21/4.33 % Propositional clauses : 0
% 25.21/4.33 % Propositional clauses after purity: 0
% 25.21/4.33 % Propositional unsat core size : 0
% 25.21/4.33 % Propositional preprocessing time : 0.000
% 25.21/4.33 % Propositional encoding time : 0.000
% 25.21/4.33 % Propositional solver time : 0.000
% 25.21/4.33 % Success case prop preproc time : 0.000
% 25.21/4.33 % Success case prop encoding time : 0.000
% 25.21/4.33 % Success case prop solver time : 0.000
% 25.21/4.33 % Current number of processed clauses : 16
% 25.21/4.33 % Positive orientable unit clauses : 3
% 25.21/4.33 % Positive unorientable unit clauses: 1
% 25.21/4.33 % Negative unit clauses : 3
% 25.21/4.33 % Non-unit-clauses : 9
% 25.21/4.33 % Current number of unprocessed clauses: 159632
% 25.21/4.33 % ...number of literals in the above : 549961
% 25.21/4.33 % Current number of archived formulas : 0
% 25.21/4.33 % Current number of archived clauses : 2939
% 25.21/4.33 % Clause-clause subsumption calls (NU) : 316259
% 25.21/4.33 % Rec. Clause-clause subsumption calls : 185365
% 25.21/4.33 % Non-unit clause-clause subsumptions : 4135
% 25.21/4.33 % Unit Clause-clause subsumption calls : 58043
% 25.21/4.33 % Rewrite failures with RHS unbound : 0
% 25.21/4.33 % BW rewrite match attempts : 7789
% 25.21/4.33 % BW rewrite match successes : 2023
% 25.21/4.33 % Condensation attempts : 0
% 25.21/4.33 % Condensation successes : 0
% 25.21/4.33 % Termbank termtop insertions : 3909108
% 25.21/4.33 % Search garbage collected termcells : 12541
% 25.21/4.33
% 25.21/4.33 % -------------------------------------------------
% 25.21/4.33 % User time : 3.483 s
% 25.21/4.33 % System time : 0.133 s
% 25.21/4.33 % Total time : 3.616 s
% 25.21/4.33 % Maximum resident set size: 7524 pages
% 25.21/4.33
% 25.21/4.33 % -------------------------------------------------
% 25.21/4.33 % User time : 16.697 s
% 25.21/4.33 % System time : 0.662 s
% 25.21/4.33 % Total time : 17.360 s
% 25.21/4.33 % Maximum resident set size: 5376 pages
% 25.21/4.33 % E exiting
%------------------------------------------------------------------------------