%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SCT043-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 22:13:10 EDT 2022
% Result : Unsatisfiable 32.74s 32.90s
% Output : Refutation 32.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 62
% Syntax : Number of clauses : 226 ( 99 unt; 36 nHn; 226 RR)
% Number of literals : 383 ( 0 equ; 154 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 15 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 15 con; 0-5 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(18,axiom,
equal(hAPP(c_Fun_Ofun__upd(u,v,w,x,y),v),w),
file('SCT043-1.p',unknown),
[] ).
cnf(19,axiom,
equal(c_Fun_Ofun__upd(u,v,hAPP(u,v),w,x),u),
file('SCT043-1.p',unknown),
[] ).
cnf(44,axiom,
equal(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool))),v),v),
file('SCT043-1.p',unknown),
[] ).
cnf(156,axiom,
equal(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool)),c_Set_Oinsert(v,c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),u)),w),c_Set_Oinsert(v,w,u)),
file('SCT043-1.p',unknown),
[] ).
cnf(180,axiom,
equal(c_Collect(hAPP(c_COMBB(c_Not,tc_bool,tc_bool,u),v),u),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),c_Collect(v,u))),
file('SCT043-1.p',unknown),
[] ).
cnf(181,axiom,
equal(c_Set_Ovimage(u,c_Collect(v,w),x,w),c_Collect(hAPP(c_COMBB(v,w,tc_bool,x),u),x)),
file('SCT043-1.p',unknown),
[] ).
cnf(241,axiom,
( ~ class_Lattices_Oupper__semilattice(u)
| equal(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(u),v),w),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(u),w),v)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(302,axiom,
equal(c_Collect(u,v),u),
file('SCT043-1.p',unknown),
[] ).
cnf(305,axiom,
~ equal(c_Set_Oinsert(u,v,w),c_Orderings_Obot__class_Obot(tc_fun(w,tc_bool))),
file('SCT043-1.p',unknown),
[] ).
cnf(308,axiom,
equal(c_Set_Oinsert(u,c_Set_Oinsert(u,v,w),w),c_Set_Oinsert(u,v,w)),
file('SCT043-1.p',unknown),
[] ).
cnf(355,axiom,
equal(hAPP(c_COMBK(u,v,w),x),u),
file('SCT043-1.p',unknown),
[] ).
cnf(362,axiom,
( ~ class_Lattices_Oboolean__algebra(u)
| equal(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(u),v),hAPP(c_HOL_Ouminus__class_Ouminus(u),w)),c_HOL_Ominus__class_Ominus(v,w,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(367,axiom,
equal(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool)),v),w),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool)),w),v)),
file('SCT043-1.p',unknown),
[] ).
cnf(376,axiom,
equal(c_Set_Ovimage(u,hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(v,tc_bool)),w),x,v),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(x,tc_bool)),c_Set_Ovimage(u,w,x,v))),
file('SCT043-1.p',unknown),
[] ).
cnf(403,axiom,
( equal(c_HOL_Ominus__class_Ominus(c_Set_Oinsert(u,v,w),c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(w,tc_bool)),w),tc_fun(w,tc_bool)),v)
| hBOOL(hAPP(hAPP(c_in(w),u),v)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(407,axiom,
equal(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v)),v),
file('SCT043-1.p',unknown),
[] ).
cnf(409,axiom,
( ~ class_Lattices_Oboolean__algebra(u)
| equal(hAPP(c_HOL_Ouminus__class_Ouminus(u),hAPP(c_HOL_Ouminus__class_Ouminus(u),v)),v) ),
file('SCT043-1.p',unknown),
[] ).
cnf(458,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),v)),
file('SCT043-1.p',unknown),
[] ).
cnf(471,axiom,
( ~ class_Lattices_Oboolean__algebra(u)
| ~ equal(hAPP(c_HOL_Ouminus__class_Ouminus(u),v),hAPP(c_HOL_Ouminus__class_Ouminus(u),w))
| equal(v,w) ),
file('SCT043-1.p',unknown),
[] ).
cnf(473,axiom,
( ~ equal(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),w))
| equal(v,w) ),
file('SCT043-1.p',unknown),
[] ).
cnf(491,axiom,
( hBOOL(hAPP(hAPP(c_in(u),v),w))
| equal(c_Set_Ovimage(c_COMBK(v,u,x),w,x,u),c_Orderings_Obot__class_Obot(tc_fun(x,tc_bool))) ),
file('SCT043-1.p',unknown),
[] ).
cnf(497,axiom,
~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_Set_Oinsert(v,w,u)),
file('SCT043-1.p',unknown),
[] ).
cnf(515,axiom,
equal(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool)),v),v),v),
file('SCT043-1.p',unknown),
[] ).
cnf(519,axiom,
equal(c_Collect(hAPP(c_COMBC(c_fequal(u),u,u,tc_bool),v),u),c_Set_Oinsert(v,c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),u)),
file('SCT043-1.p',unknown),
[] ).
cnf(526,axiom,
( ~ hBOOL(hAPP(c_Set_Ovimage(u,v,w,x),y))
| hBOOL(hAPP(v,hAPP(u,y))) ),
file('SCT043-1.p',unknown),
[] ).
cnf(527,axiom,
( ~ hBOOL(hAPP(u,hAPP(v,w)))
| hBOOL(hAPP(c_Set_Ovimage(v,u,x,y),w)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(531,axiom,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),c_Collect(hAPP(c_fequal(v),u),v)),
file('SCT043-1.p',unknown),
[] ).
cnf(532,axiom,
equal(c_Set_Ovimage(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),w,v),c_Orderings_Obot__class_Obot(tc_fun(w,tc_bool))),
file('SCT043-1.p',unknown),
[] ).
cnf(533,axiom,
equal(c_Collect(hAPP(c_COMBC(c_in(u),u,tc_fun(u,tc_bool),tc_bool),v),u),v),
file('SCT043-1.p',unknown),
[] ).
cnf(549,axiom,
( hBOOL(hAPP(hAPP(c_in(u),v),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),w)))
| hBOOL(hAPP(hAPP(c_in(u),v),w)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(550,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(u),v),w))
| ~ hBOOL(hAPP(hAPP(c_in(u),v),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),w))) ),
file('SCT043-1.p',unknown),
[] ).
cnf(604,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(u),v),w))
| equal(c_Set_Oinsert(v,w,u),w) ),
file('SCT043-1.p',unknown),
[] ).
cnf(641,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(u),v),w))
| hBOOL(hAPP(w,v)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(645,axiom,
hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_P____),c_Arrow__Order__Mirabelle_OProf)),
file('SCT043-1.p',unknown),
[] ).
cnf(647,axiom,
( ~ class_Complete__Lattice_Ocomplete__lattice(u)
| class_Complete__Lattice_Ocomplete__lattice(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(648,axiom,
( ~ class_Lattices_Olattice(u)
| class_Lattices_Oupper__semilattice(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(649,axiom,
( ~ class_Lattices_Olattice(u)
| class_Lattices_Olower__semilattice(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(650,axiom,
( ~ class_Lattices_Odistrib__lattice(u)
| class_Lattices_Odistrib__lattice(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(651,axiom,
( ~ class_Lattices_Obounded__lattice(u)
| class_Lattices_Obounded__lattice(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(652,axiom,
( ~ class_Lattices_Oboolean__algebra(u)
| class_Lattices_Oboolean__algebra(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(654,axiom,
( ~ class_Orderings_Opreorder(u)
| class_Orderings_Opreorder(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(655,axiom,
( ~ class_Lattices_Olattice(u)
| class_Lattices_Olattice(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(656,axiom,
( ~ class_Orderings_Oorder(u)
| class_Orderings_Oorder(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(657,axiom,
( ~ class_Orderings_Obot(u)
| class_Orderings_Obot(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(658,axiom,
( ~ class_HOL_Oord(u)
| class_HOL_Oord(tc_fun(v,u)) ),
file('SCT043-1.p',unknown),
[] ).
cnf(672,axiom,
class_Complete__Lattice_Ocomplete__lattice(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(673,axiom,
class_Lattices_Oupper__semilattice(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(674,axiom,
class_Lattices_Olower__semilattice(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(675,axiom,
class_Lattices_Odistrib__lattice(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(676,axiom,
class_Lattices_Obounded__lattice(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(677,axiom,
class_Lattices_Oboolean__algebra(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(678,axiom,
class_Finite__Set_Ofinite_Ofinite(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(679,axiom,
class_Orderings_Opreorder(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(680,axiom,
class_Lattices_Olattice(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(681,axiom,
class_Orderings_Oorder(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(682,axiom,
class_Orderings_Obot(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(683,axiom,
class_HOL_Oord(tc_bool),
file('SCT043-1.p',unknown),
[] ).
cnf(684,axiom,
equal(hAPP(hAPP(c_COMBC(u,v,w,x),y),z),hAPP(hAPP(u,z),y)),
file('SCT043-1.p',unknown),
[] ).
cnf(685,axiom,
equal(hAPP(hAPP(c_COMBB(u,v,w,x),y),z),hAPP(u,hAPP(y,z))),
file('SCT043-1.p',unknown),
[] ).
cnf(686,axiom,
hBOOL(hAPP(hAPP(c_fequal(u),v),v)),
file('SCT043-1.p',unknown),
[] ).
cnf(687,axiom,
( ~ hBOOL(hAPP(hAPP(c_fequal(u),v),w))
| equal(v,w) ),
file('SCT043-1.p',unknown),
[] ).
cnf(688,axiom,
~ hBOOL(hAPP(hAPP(c_in(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____)),c_Arrow__Order__Mirabelle_OProf)),
file('SCT043-1.p',unknown),
[] ).
cnf(691,plain,
equal(hAPP(c_COMBC(c_in(u),u,tc_fun(u,tc_bool),tc_bool),v),v),
inference(rew,[status(thm),theory(equality)],[302,533]),
[iquote('0:Rew:302.0,533.0')] ).
cnf(692,plain,
equal(c_Set_Oinsert(u,c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),v),hAPP(c_fequal(v),u)),
inference(rew,[status(thm),theory(equality)],[302,531]),
[iquote('0:Rew:302.0,531.0')] ).
cnf(697,plain,
equal(hAPP(c_COMBB(u,v,tc_bool,w),x),c_Set_Ovimage(x,u,w,v)),
inference(rew,[status(thm),theory(equality)],[302,181]),
[iquote('0:Rew:302.0,181.0,302.0,181.0')] ).
cnf(698,plain,
equal(hAPP(c_COMBC(c_fequal(u),u,u,tc_bool),v),hAPP(c_fequal(u),v)),
inference(rew,[status(thm),theory(equality)],[302,519,692]),
[iquote('0:Rew:302.0,519.0,692.0,519.0')] ).
cnf(700,plain,
equal(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v),c_Set_Ovimage(v,c_Not,u,tc_bool)),
inference(rew,[status(thm),theory(equality)],[302,180,697]),
[iquote('0:Rew:302.0,180.0,697.0,180.0,302.0,180.0')] ).
cnf(701,plain,
( ~ equal(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v),c_Set_Ovimage(w,c_Not,u,tc_bool))
| equal(v,w) ),
inference(rew,[status(thm),theory(equality)],[700,473]),
[iquote('0:Rew:700.0,473.0')] ).
cnf(702,plain,
equal(c_Set_Ovimage(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v),c_Not,u,tc_bool),v),
inference(rew,[status(thm),theory(equality)],[700,407]),
[iquote('0:Rew:700.0,407.0')] ).
cnf(704,plain,
equal(c_Set_Ovimage(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not,v,tc_bool),u),
inference(rew,[status(thm),theory(equality)],[700,702]),
[iquote('0:Rew:700.0,702.0')] ).
cnf(705,plain,
( ~ equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Set_Ovimage(w,c_Not,v,tc_bool))
| equal(u,w) ),
inference(rew,[status(thm),theory(equality)],[700,701]),
[iquote('0:Rew:700.0,701.0')] ).
cnf(707,plain,
( hBOOL(hAPP(hAPP(c_in(u),v),w))
| hBOOL(hAPP(hAPP(c_in(u),v),c_Set_Ovimage(w,c_Not,u,tc_bool))) ),
inference(rew,[status(thm),theory(equality)],[700,549]),
[iquote('0:Rew:700.0,549.0')] ).
cnf(710,plain,
equal(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool)),hAPP(c_fequal(u),v)),w),c_Set_Oinsert(v,w,u)),
inference(rew,[status(thm),theory(equality)],[692,156]),
[iquote('0:Rew:692.0,156.0')] ).
cnf(716,plain,
equal(c_Set_Ovimage(u,c_Set_Ovimage(v,c_Not,w,tc_bool),x,w),c_Set_Ovimage(c_Set_Ovimage(u,v,x,w),c_Not,x,tc_bool)),
inference(rew,[status(thm),theory(equality)],[700,376]),
[iquote('0:Rew:700.0,376.0,700.0,376.0')] ).
cnf(717,plain,
equal(c_Set_Ovimage(u,c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),v,tc_bool),u),
inference(rew,[status(thm),theory(equality)],[716,704]),
[iquote('0:Rew:716.0,704.0')] ).
cnf(719,plain,
( ~ hBOOL(hAPP(hAPP(c_in(u),v),w))
| ~ hBOOL(hAPP(hAPP(c_in(u),v),c_Set_Ovimage(w,c_Not,u,tc_bool))) ),
inference(rew,[status(thm),theory(equality)],[700,550]),
[iquote('0:Rew:700.0,550.1')] ).
cnf(735,plain,
( hBOOL(hAPP(hAPP(c_in(u),v),w))
| equal(c_HOL_Ominus__class_Ominus(c_Set_Oinsert(v,w,u),hAPP(c_fequal(u),v),tc_fun(u,tc_bool)),w) ),
inference(rew,[status(thm),theory(equality)],[692,403]),
[iquote('0:Rew:692.0,403.0')] ).
cnf(834,plain,
equal(c_HOL_Ominus__class_Ominus(c_Set_Oinsert(hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),hAPP(c_fequal(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____)),tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_bool)),c_Arrow__Order__Mirabelle_OProf),
inference(res,[status(thm),theory(equality)],[735,688]),
[iquote('0:Res:735.1,688.0')] ).
cnf(924,plain,
~ equal(hAPP(c_fequal(u),v),c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool))),
inference(spl,[status(thm),theory(equality)],[692,497]),
[iquote('0:SpL:692.0,497.0')] ).
cnf(1003,plain,
equal(c_Set_Oinsert(u,hAPP(c_fequal(v),u),v),hAPP(c_fequal(v),u)),
inference(spr,[status(thm),theory(equality)],[692,308]),
[iquote('0:SpR:692.0,308.0')] ).
cnf(1018,plain,
hBOOL(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),
inference(res,[status(thm),theory(equality)],[645,641]),
[iquote('0:Res:645.0,641.0')] ).
cnf(1129,plain,
equal(c_Set_Oinsert(v_P____,c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),c_Arrow__Order__Mirabelle_OProf),
inference(res,[status(thm),theory(equality)],[645,604]),
[iquote('0:Res:645.0,604.0')] ).
cnf(1303,plain,
( ~ hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),hAPP(u,v)))
| hBOOL(hAPP(u,v)) ),
inference(spr,[status(thm),theory(equality)],[717,527]),
[iquote('0:SpR:717.0,527.1')] ).
cnf(1315,plain,
( ~ hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),u))
| hBOOL(hAPP(c_COMBK(u,v,w),x)) ),
inference(spl,[status(thm),theory(equality)],[355,1303]),
[iquote('0:SpL:355.0,1303.0')] ).
cnf(1328,plain,
( ~ hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),u))
| hBOOL(u) ),
inference(rew,[status(thm),theory(equality)],[355,1315]),
[iquote('0:Rew:355.0,1315.1')] ).
cnf(1351,plain,
( ~ hBOOL(hAPP(u,v))
| hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),hAPP(u,v))) ),
inference(spl,[status(thm),theory(equality)],[717,526]),
[iquote('0:SpL:717.0,526.0')] ).
cnf(1364,plain,
( ~ hBOOL(hAPP(c_COMBK(u,v,w),x))
| hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),u)) ),
inference(spr,[status(thm),theory(equality)],[355,1351]),
[iquote('0:SpR:355.0,1351.1')] ).
cnf(1378,plain,
( ~ hBOOL(u)
| hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),u)) ),
inference(rew,[status(thm),theory(equality)],[355,1364]),
[iquote('0:Rew:355.0,1364.0')] ).
cnf(1436,plain,
equal(hAPP(hAPP(c_in(u),v),w),hAPP(w,v)),
inference(spr,[status(thm),theory(equality)],[691,684]),
[iquote('0:SpR:691.0,684.0')] ).
cnf(1437,plain,
equal(hAPP(hAPP(c_fequal(u),v),w),hAPP(hAPP(c_fequal(u),w),v)),
inference(spr,[status(thm),theory(equality)],[698,684]),
[iquote('0:SpR:698.0,684.0')] ).
cnf(1555,plain,
( ~ hBOOL(hAPP(hAPP(c_in(u),v),w))
| ~ hBOOL(hAPP(c_Set_Ovimage(w,c_Not,u,tc_bool),v)) ),
inference(rew,[status(thm),theory(equality)],[1436,719]),
[iquote('0:Rew:1436.0,719.1')] ).
cnf(1556,plain,
( hBOOL(hAPP(hAPP(c_in(u),v),w))
| hBOOL(hAPP(c_Set_Ovimage(w,c_Not,u,tc_bool),v)) ),
inference(rew,[status(thm),theory(equality)],[1436,707]),
[iquote('0:Rew:1436.0,707.1')] ).
cnf(1613,plain,
( hBOOL(hAPP(u,v))
| equal(c_Set_Ovimage(c_COMBK(v,w,x),u,x,w),c_Orderings_Obot__class_Obot(tc_fun(x,tc_bool))) ),
inference(rew,[status(thm),theory(equality)],[1436,491]),
[iquote('0:Rew:1436.0,491.0')] ).
cnf(1616,plain,
( hBOOL(hAPP(u,v))
| hBOOL(hAPP(c_Set_Ovimage(u,c_Not,w,tc_bool),v)) ),
inference(rew,[status(thm),theory(equality)],[1436,1556]),
[iquote('0:Rew:1436.0,1556.0')] ).
cnf(1618,plain,
( ~ hBOOL(hAPP(u,v))
| ~ hBOOL(hAPP(c_Set_Ovimage(u,c_Not,w,tc_bool),v)) ),
inference(rew,[status(thm),theory(equality)],[1436,1555]),
[iquote('0:Rew:1436.0,1555.0')] ).
cnf(1675,plain,
( hBOOL(hAPP(c_Not,u))
| hBOOL(u) ),
inference(res,[status(thm),theory(equality)],[1616,1328]),
[iquote('0:Res:1616.1,1328.0')] ).
cnf(1716,plain,
( ~ hBOOL(u)
| ~ hBOOL(hAPP(c_Not,u)) ),
inference(res,[status(thm),theory(equality)],[1378,1618]),
[iquote('0:Res:1378.1,1618.1')] ).
cnf(1835,plain,
equal(hAPP(c_Set_Ovimage(u,v,w,x),y),hAPP(v,hAPP(u,y))),
inference(spr,[status(thm),theory(equality)],[697,685]),
[iquote('0:SpR:697.0,685.0')] ).
cnf(1901,plain,
equal(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),hAPP(u,v)),hAPP(u,v)),
inference(spr,[status(thm),theory(equality)],[717,1835]),
[iquote('0:SpR:717.0,1835.0')] ).
cnf(1902,plain,
equal(hAPP(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),v),hAPP(c_Orderings_Obot__class_Obot(tc_fun(w,tc_bool)),hAPP(x,v))),
inference(spr,[status(thm),theory(equality)],[532,1835]),
[iquote('0:SpR:532.0,1835.0')] ).
cnf(1904,plain,
equal(hAPP(c_Not,hAPP(c_Not,hAPP(u,v))),hAPP(u,v)),
inference(rew,[status(thm),theory(equality)],[1835,1901]),
[iquote('0:Rew:1835.0,1901.0')] ).
cnf(1913,plain,
equal(hAPP(c_Not,hAPP(c_Not,u)),u),
inference(spr,[status(thm),theory(equality)],[515,1904]),
[iquote('0:SpR:515.0,1904.0')] ).
cnf(1946,plain,
equal(c_Fun_Ofun__upd(c_Not,hAPP(c_Not,u),u,v,w),c_Not),
inference(spr,[status(thm),theory(equality)],[1913,19]),
[iquote('0:SpR:1913.0,19.0')] ).
cnf(2067,plain,
equal(hAPP(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),v),hAPP(c_Orderings_Obot__class_Obot(tc_fun(w,tc_bool)),x)),
inference(spr,[status(thm),theory(equality)],[18,1902]),
[iquote('0:SpR:18.0,1902.0')] ).
cnf(2591,plain,
( ~ class_Lattices_Oupper__semilattice(tc_fun(u,tc_bool))
| equal(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool)),v),hAPP(c_fequal(u),w)),c_Set_Oinsert(w,v,u)) ),
inference(spr,[status(thm),theory(equality)],[241,710]),
[iquote('0:SpR:241.1,710.0')] ).
cnf(2604,plain,
equal(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool)),v),hAPP(c_fequal(u),w)),c_Set_Oinsert(w,v,u)),
inference(ssi,[status(thm)],[2591,657,682,672,683,678,675,676,677,681,679,674,673,680,647,658,650,651,652,656,654,649,648,655]),
[iquote('0:SSi:2591.0,657.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,647.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,658.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,650.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,651.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,652.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,656.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,654.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,649.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,648.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,655.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1')] ).
cnf(2741,plain,
( ~ class_Lattices_Oboolean__algebra(u)
| ~ class_Lattices_Oboolean__algebra(u)
| ~ equal(v,hAPP(c_HOL_Ouminus__class_Ouminus(u),w))
| equal(hAPP(c_HOL_Ouminus__class_Ouminus(u),v),w) ),
inference(spl,[status(thm),theory(equality)],[409,471]),
[iquote('0:SpL:409.1,471.1')] ).
cnf(2750,plain,
( ~ class_Lattices_Oboolean__algebra(u)
| ~ equal(v,hAPP(c_HOL_Ouminus__class_Ouminus(u),w))
| equal(hAPP(c_HOL_Ouminus__class_Ouminus(u),v),w) ),
inference(obv,[status(thm),theory(equality)],[2741]),
[iquote('0:Obv:2741.0')] ).
cnf(3207,plain,
( ~ class_Lattices_Oboolean__algebra(u)
| ~ class_Lattices_Oboolean__algebra(u)
| ~ equal(v,w)
| equal(hAPP(c_HOL_Ouminus__class_Ouminus(u),v),hAPP(c_HOL_Ouminus__class_Ouminus(u),w)) ),
inference(spl,[status(thm),theory(equality)],[409,2750]),
[iquote('0:SpL:409.1,2750.1')] ).
cnf(3211,plain,
( ~ class_Lattices_Oboolean__algebra(u)
| ~ equal(v,w)
| equal(hAPP(c_HOL_Ouminus__class_Ouminus(u),v),hAPP(c_HOL_Ouminus__class_Ouminus(u),w)) ),
inference(obv,[status(thm),theory(equality)],[3207]),
[iquote('0:Obv:3207.0')] ).
cnf(3412,plain,
( ~ class_Lattices_Oboolean__algebra(tc_fun(u,tc_bool))
| ~ equal(v,w)
| equal(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v),c_Set_Ovimage(w,c_Not,u,tc_bool)) ),
inference(spr,[status(thm),theory(equality)],[3211,700]),
[iquote('0:SpR:3211.2,700.0')] ).
cnf(3448,plain,
( ~ class_Lattices_Oboolean__algebra(tc_fun(u,tc_bool))
| ~ equal(v,w)
| equal(c_Set_Ovimage(v,c_Not,u,tc_bool),c_Set_Ovimage(w,c_Not,u,tc_bool)) ),
inference(rew,[status(thm),theory(equality)],[700,3412]),
[iquote('0:Rew:700.0,3412.2')] ).
cnf(3449,plain,
( ~ equal(u,v)
| equal(c_Set_Ovimage(u,c_Not,w,tc_bool),c_Set_Ovimage(v,c_Not,w,tc_bool)) ),
inference(ssi,[status(thm)],[3448,657,682,672,683,678,675,676,677,681,679,674,673,680,647,658,650,651,652,656,654,649,648,655]),
[iquote('0:SSi:3448.0,657.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,647.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,658.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,650.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,651.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,652.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,656.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,654.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,649.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,648.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,655.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1')] ).
cnf(3509,plain,
( ~ equal(u,v)
| equal(hAPP(c_Set_Ovimage(v,c_Not,w,tc_bool),x),hAPP(c_Not,hAPP(u,x))) ),
inference(spr,[status(thm),theory(equality)],[3449,1835]),
[iquote('0:SpR:3449.1,1835.0')] ).
cnf(3528,plain,
( ~ equal(u,v)
| equal(hAPP(c_Not,hAPP(v,w)),hAPP(c_Not,hAPP(u,w))) ),
inference(rew,[status(thm),theory(equality)],[1835,3509]),
[iquote('0:Rew:1835.0,3509.1')] ).
cnf(3556,plain,
( ~ equal(u,v)
| equal(hAPP(c_Not,hAPP(c_Not,hAPP(u,w))),hAPP(v,w)) ),
inference(spr,[status(thm),theory(equality)],[3528,1913]),
[iquote('0:SpR:3528.1,1913.0')] ).
cnf(3559,plain,
( ~ equal(u,c_Not)
| equal(hAPP(c_Not,hAPP(u,v)),v) ),
inference(spr,[status(thm),theory(equality)],[3528,1913]),
[iquote('0:SpR:3528.1,1913.0')] ).
cnf(3705,plain,
( ~ equal(u,v)
| equal(hAPP(u,w),hAPP(v,w)) ),
inference(rew,[status(thm),theory(equality)],[1913,3556]),
[iquote('0:Rew:1913.0,3556.1')] ).
cnf(3718,plain,
( ~ equal(u,c_Not)
| hBOOL(v)
| hBOOL(hAPP(u,v)) ),
inference(spr,[status(thm),theory(equality)],[3559,1675]),
[iquote('0:SpR:3559.1,1675.0')] ).
cnf(3739,plain,
( ~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_Not)
| equal(hAPP(c_Not,hAPP(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),w)),x) ),
inference(spr,[status(thm),theory(equality)],[2067,3559]),
[iquote('0:SpR:2067.0,3559.1')] ).
cnf(3741,plain,
( ~ equal(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),c_Not)
| equal(hAPP(c_Not,c_Set_Ovimage(v,c_Not,u,tc_bool)),v) ),
inference(spr,[status(thm),theory(equality)],[700,3559]),
[iquote('0:SpR:700.0,3559.1')] ).
cnf(3794,plain,
( ~ equal(u,c_Not)
| ~ hBOOL(hAPP(u,v))
| ~ hBOOL(v) ),
inference(spl,[status(thm),theory(equality)],[3559,1716]),
[iquote('0:SpL:3559.1,1716.1')] ).
cnf(3797,plain,
~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_Not),
inference(aed,[status(thm),theory(equality)],[305,3739]),
[iquote('0:AED:305.0,3739.1')] ).
cnf(3887,plain,
( ~ equal(hAPP(c_in(u),v),c_Not)
| hBOOL(w)
| hBOOL(hAPP(w,v)) ),
inference(spr,[status(thm),theory(equality)],[1436,3718]),
[iquote('0:SpR:1436.0,3718.2')] ).
cnf(4118,plain,
( ~ equal(c_Not,u)
| equal(hAPP(u,hAPP(c_Not,v)),v) ),
inference(spr,[status(thm),theory(equality)],[3705,1913]),
[iquote('0:SpR:3705.1,1913.0')] ).
cnf(4121,plain,
( ~ equal(c_Arrow__Order__Mirabelle_OProf,u)
| hBOOL(hAPP(u,v_P____)) ),
inference(spr,[status(thm),theory(equality)],[3705,1018]),
[iquote('0:SpR:3705.1,1018.0')] ).
cnf(4536,plain,
~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_Arrow__Order__Mirabelle_OProf),
inference(res,[status(thm),theory(equality)],[4121,458]),
[iquote('0:Res:4121.1,458.0')] ).
cnf(4541,plain,
( ~ equal(hAPP(c_fequal(u),v),c_Arrow__Order__Mirabelle_OProf)
| equal(v,v_P____) ),
inference(res,[status(thm),theory(equality)],[4121,687]),
[iquote('0:Res:4121.1,687.0')] ).
cnf(4592,plain,
( ~ equal(u,c_fequal(v))
| ~ equal(hAPP(u,w),c_Arrow__Order__Mirabelle_OProf)
| equal(w,v_P____) ),
inference(spl,[status(thm),theory(equality)],[3705,4541]),
[iquote('0:SpL:3705.1,4541.0')] ).
cnf(5099,plain,
( ~ equal(c_fequal(u),c_Not)
| ~ equal(v,c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool))) ),
inference(spl,[status(thm),theory(equality)],[4118,924]),
[iquote('0:SpL:4118.1,924.0')] ).
cnf(5150,plain,
~ equal(c_fequal(u),c_Not),
inference(aed,[status(thm),theory(equality)],[305,5099]),
[iquote('0:AED:305.0,5099.1')] ).
cnf(5622,plain,
( ~ equal(hAPP(c_in(u),v),c_Not)
| ~ hBOOL(hAPP(w,v))
| ~ hBOOL(w) ),
inference(spl,[status(thm),theory(equality)],[1436,3794]),
[iquote('0:SpL:1436.0,3794.1')] ).
cnf(5634,plain,
( ~ equal(hAPP(c_fequal(u),v),c_Not)
| ~ hBOOL(v) ),
inference(res,[status(thm),theory(equality)],[686,3794]),
[iquote('0:Res:686.0,3794.1')] ).
cnf(5719,plain,
( ~ equal(u,c_fequal(v))
| ~ equal(hAPP(u,w),c_Not)
| ~ hBOOL(w) ),
inference(spl,[status(thm),theory(equality)],[3705,5634]),
[iquote('0:SpL:3705.1,5634.0')] ).
cnf(6825,plain,
( ~ class_Lattices_Oboolean__algebra(tc_fun(u,tc_bool))
| equal(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool)),hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v)),w),c_HOL_Ominus__class_Ominus(w,v,tc_fun(u,tc_bool))) ),
inference(spr,[status(thm),theory(equality)],[362,367]),
[iquote('0:SpR:362.1,367.0')] ).
cnf(6878,plain,
( ~ class_Lattices_Oboolean__algebra(tc_fun(u,tc_bool))
| equal(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool)),c_Set_Ovimage(v,c_Not,u,tc_bool)),w),c_HOL_Ominus__class_Ominus(w,v,tc_fun(u,tc_bool))) ),
inference(rew,[status(thm),theory(equality)],[700,6825]),
[iquote('0:Rew:700.0,6825.1')] ).
cnf(6879,plain,
equal(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool)),c_Set_Ovimage(v,c_Not,u,tc_bool)),w),c_HOL_Ominus__class_Ominus(w,v,tc_fun(u,tc_bool))),
inference(ssi,[status(thm)],[6878,657,682,672,683,678,675,676,677,681,679,674,673,680,647,658,650,651,652,656,654,649,648,655]),
[iquote('0:SSi:6878.0,657.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,647.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,658.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,650.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,651.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,652.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,656.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,654.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,649.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,648.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1,655.0,682.0,672.0,683.0,678.0,675.0,676.0,677.0,681.0,679.0,674.0,673.0,680.1')] ).
cnf(9694,plain,
( ~ equal(c_COMBK(u,v,w),c_fequal(x))
| ~ equal(u,c_Arrow__Order__Mirabelle_OProf)
| equal(y,v_P____) ),
inference(spl,[status(thm),theory(equality)],[355,4592]),
[iquote('0:SpL:355.0,4592.1')] ).
cnf(9754,plain,
( ~ equal(c_COMBK(u,v,w),c_fequal(x))
| ~ equal(u,c_Arrow__Order__Mirabelle_OProf) ),
inference(aed,[status(thm),theory(equality)],[305,9694]),
[iquote('0:AED:305.0,9694.2')] ).
cnf(11398,plain,
( hBOOL(hAPP(c_Set_Ovimage(c_Not,c_Not,tc_bool,tc_bool),u))
| equal(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),c_COMBK(u,tc_bool,v)) ),
inference(spr,[status(thm),theory(equality)],[1613,717]),
[iquote('0:SpR:1613.1,717.0')] ).
cnf(11411,plain,
( hBOOL(u)
| equal(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),c_COMBK(u,tc_bool,v)) ),
inference(rew,[status(thm),theory(equality)],[1913,11398,1835]),
[iquote('0:Rew:1913.0,11398.0,1835.0,11398.0')] ).
cnf(11458,plain,
( hBOOL(u)
| equal(hAPP(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),w),u) ),
inference(spr,[status(thm),theory(equality)],[11411,355]),
[iquote('0:SpR:11411.1,355.0')] ).
cnf(11490,plain,
( ~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_fequal(v))
| ~ equal(w,c_Arrow__Order__Mirabelle_OProf)
| hBOOL(w) ),
inference(spl,[status(thm),theory(equality)],[11411,9754]),
[iquote('0:SpL:11411.1,9754.0')] ).
cnf(11521,plain,
( hBOOL(u)
| hBOOL(v)
| equal(u,v) ),
inference(spr,[status(thm),theory(equality)],[11458]),
[iquote('0:SpR:11458.1,11458.1')] ).
cnf(12208,plain,
( ~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_fequal(v))
| ~ equal(w,c_Not)
| ~ hBOOL(x)
| hBOOL(w) ),
inference(spl,[status(thm),theory(equality)],[11458,5719]),
[iquote('0:SpL:11458.1,5719.1')] ).
cnf(14226,plain,
( ~ hBOOL(hAPP(u,v))
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(w,tc_bool)))
| hBOOL(u) ),
inference(spl,[status(thm),theory(equality)],[11521,458]),
[iquote('0:SpL:11521.2,458.0')] ).
cnf(14230,plain,
( ~ equal(u,c_Not)
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)))
| hBOOL(u) ),
inference(spl,[status(thm),theory(equality)],[11521,3797]),
[iquote('0:SpL:11521.2,3797.0')] ).
cnf(14260,plain,
( ~ equal(u,c_Not)
| hBOOL(c_fequal(v))
| hBOOL(u) ),
inference(spl,[status(thm),theory(equality)],[11521,5150]),
[iquote('0:SpL:11521.2,5150.0')] ).
cnf(15105,plain,
( ~ hBOOL(u)
| hBOOL(v)
| equal(hAPP(c_Not,u),v) ),
inference(res,[status(thm),theory(equality)],[11521,1716]),
[iquote('0:Res:11521.0,1716.1')] ).
cnf(15886,plain,
( ~ equal(u,c_Not)
| hBOOL(u) ),
inference(spt,[spt(split,[position(s1)])],[14260]),
[iquote('1:Spt:14260.0,14260.2')] ).
cnf(15927,plain,
( ~ equal(hAPP(c_Not,u),c_Not)
| ~ hBOOL(u) ),
inference(res,[status(thm),theory(equality)],[15886,1716]),
[iquote('1:Res:15886.1,1716.1')] ).
cnf(16152,plain,
( ~ equal(u,c_Not)
| ~ hBOOL(hAPP(c_Not,u)) ),
inference(spl,[status(thm),theory(equality)],[1913,15927]),
[iquote('1:SpL:1913.0,15927.0')] ).
cnf(16405,plain,
( hBOOL(u)
| equal(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),u) ),
inference(res,[status(thm),theory(equality)],[1018,15105]),
[iquote('0:Res:1018.0,15105.0')] ).
cnf(16772,plain,
( hBOOL(hAPP(c_Not,u))
| equal(hAPP(c_Not,hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____))),u) ),
inference(spr,[status(thm),theory(equality)],[16405,1913]),
[iquote('0:SpR:16405.1,1913.0')] ).
cnf(17333,plain,
equal(hAPP(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),v),hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____))),
inference(res,[status(thm),theory(equality)],[16405,458]),
[iquote('0:Res:16405.0,458.0')] ).
cnf(17403,plain,
~ hBOOL(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____))),
inference(rew,[status(thm),theory(equality)],[17333,458]),
[iquote('0:Rew:17333.0,458.0')] ).
cnf(18314,plain,
( hBOOL(hAPP(c_Not,u))
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),u) ),
inference(rew,[status(thm),theory(equality)],[1913,16772]),
[iquote('0:Rew:1913.0,16772.1')] ).
cnf(19176,plain,
( ~ equal(u,c_Not)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),u) ),
inference(res,[status(thm),theory(equality)],[18314,16152]),
[iquote('1:Res:18314.0,16152.1')] ).
cnf(19177,plain,
( ~ hBOOL(u)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),u) ),
inference(res,[status(thm),theory(equality)],[18314,1716]),
[iquote('0:Res:18314.0,1716.1')] ).
cnf(19255,plain,
( equal(hAPP(c_Not,hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),u)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),u) ),
inference(res,[status(thm),theory(equality)],[16405,19177]),
[iquote('0:Res:16405.0,19177.0')] ).
cnf(19561,plain,
( ~ equal(hAPP(hAPP(c_fequal(u),v),w),c_Not)
| equal(hAPP(hAPP(c_fequal(u),w),v),hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)) ),
inference(spr,[status(thm),theory(equality)],[19176,1437]),
[iquote('1:SpR:19176.1,1437.0')] ).
cnf(19820,plain,
( ~ equal(c_Fun_Ofun__upd(c_Not,hAPP(c_Not,u),u,v,w),c_Not)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),c_Not) ),
inference(spr,[status(thm),theory(equality)],[19176,1946]),
[iquote('1:SpR:19176.1,1946.0')] ).
cnf(20195,plain,
( ~ equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not)
| ~ equal(c_Set_Ovimage(w,c_Not,v,tc_bool),hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____))
| equal(u,w) ),
inference(spl,[status(thm),theory(equality)],[19176,705]),
[iquote('1:SpL:19176.1,705.0')] ).
cnf(20245,plain,
( ~ equal(c_Not,c_Not)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),c_Not) ),
inference(rew,[status(thm),theory(equality)],[1946,19820]),
[iquote('1:Rew:1946.0,19820.0')] ).
cnf(20246,plain,
equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),c_Not),
inference(obv,[status(thm),theory(equality)],[20245]),
[iquote('1:Obv:20245.0')] ).
cnf(20249,plain,
~ hBOOL(hAPP(c_Not,c_Not)),
inference(rew,[status(thm),theory(equality)],[20246,17403]),
[iquote('1:Rew:20246.0,17403.0')] ).
cnf(20602,plain,
( equal(hAPP(c_Not,c_Not),u)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),u) ),
inference(rew,[status(thm),theory(equality)],[20246,19255]),
[iquote('1:Rew:20246.0,19255.0')] ).
cnf(21434,plain,
( equal(hAPP(c_Not,c_Not),u)
| equal(c_Not,u) ),
inference(rew,[status(thm),theory(equality)],[20246,20602]),
[iquote('1:Rew:20246.0,20602.1')] ).
cnf(21741,plain,
( ~ equal(hAPP(hAPP(c_fequal(u),v),w),c_Not)
| equal(hAPP(hAPP(c_fequal(u),w),v),c_Not) ),
inference(rew,[status(thm),theory(equality)],[20246,19561]),
[iquote('1:Rew:20246.0,19561.1')] ).
cnf(21885,plain,
( ~ equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not)
| ~ equal(c_Set_Ovimage(w,c_Not,v,tc_bool),c_Not)
| equal(u,w) ),
inference(rew,[status(thm),theory(equality)],[20246,20195]),
[iquote('1:Rew:20246.0,20195.1')] ).
cnf(22697,plain,
( equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_Not)
| hBOOL(v)
| equal(c_COMBK(v,tc_bool,u),hAPP(c_Not,c_Not)) ),
inference(spr,[status(thm),theory(equality)],[21434,11411]),
[iquote('1:SpR:21434.0,11411.1')] ).
cnf(22796,plain,
( equal(hAPP(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),v),c_Not)
| equal(c_Set_Ovimage(v,c_Not,u,tc_bool),hAPP(c_Not,c_Not)) ),
inference(spr,[status(thm),theory(equality)],[21434,700]),
[iquote('1:SpR:21434.0,700.0')] ).
cnf(22804,plain,
( equal(hAPP(c_in(u),v),c_Not)
| equal(hAPP(hAPP(c_Not,c_Not),w),hAPP(w,v)) ),
inference(spr,[status(thm),theory(equality)],[21434,1436]),
[iquote('1:SpR:21434.0,1436.0')] ).
cnf(23095,plain,
( equal(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),c_Not)
| equal(hAPP(hAPP(c_Not,c_Not),v),c_Set_Ovimage(v,c_Not,u,tc_bool)) ),
inference(spr,[status(thm),theory(equality)],[21434,700]),
[iquote('1:SpR:21434.0,700.0')] ).
cnf(23190,plain,
( ~ equal(hAPP(c_Not,c_Not),c_Arrow__Order__Mirabelle_OProf)
| equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_Not) ),
inference(spl,[status(thm),theory(equality)],[21434,4536]),
[iquote('1:SpL:21434.0,4536.0')] ).
cnf(23516,plain,
~ equal(hAPP(c_Not,c_Not),c_Arrow__Order__Mirabelle_OProf),
inference(mrr,[status(thm)],[23190,3797]),
[iquote('1:MRR:23190.1,3797.0')] ).
cnf(23646,plain,
( hBOOL(u)
| equal(c_COMBK(u,tc_bool,v),hAPP(c_Not,c_Not)) ),
inference(mrr,[status(thm)],[22697,3797]),
[iquote('1:MRR:22697.0,3797.0')] ).
cnf(23647,plain,
( hBOOL(u)
| equal(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool)),hAPP(c_Not,c_Not)) ),
inference(rew,[status(thm),theory(equality)],[23646,11411]),
[iquote('1:Rew:23646.1,11411.1')] ).
cnf(23725,plain,
( ~ hBOOL(hAPP(u,v))
| hBOOL(hAPP(c_Not,c_Not))
| hBOOL(u) ),
inference(rew,[status(thm),theory(equality)],[23647,14226]),
[iquote('1:Rew:23647.1,14226.1')] ).
cnf(23819,plain,
( ~ hBOOL(hAPP(u,v))
| hBOOL(u) ),
inference(mrr,[status(thm)],[23725,20249]),
[iquote('1:MRR:23725.1,20249.0')] ).
cnf(23820,plain,
( ~ equal(hAPP(c_in(u),v),c_Not)
| hBOOL(w) ),
inference(mrr,[status(thm)],[3887,23819]),
[iquote('1:MRR:3887.2,23819.0')] ).
cnf(23833,plain,
( ~ equal(hAPP(c_in(u),v),c_Not)
| ~ hBOOL(hAPP(w,v)) ),
inference(mrr,[status(thm)],[5622,23819]),
[iquote('1:MRR:5622.2,23819.1')] ).
cnf(23856,plain,
~ equal(hAPP(c_in(u),v),c_Not),
inference(mrr,[status(thm)],[23833,23820]),
[iquote('1:MRR:23833.1,23820.1')] ).
cnf(23857,plain,
equal(hAPP(hAPP(c_Not,c_Not),u),hAPP(u,v)),
inference(mrr,[status(thm)],[22804,23856]),
[iquote('1:MRR:22804.0,23856.0')] ).
cnf(23874,plain,
equal(hAPP(hAPP(c_Not,c_Not),hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool)),v)),c_Set_Oinsert(w,v,u)),
inference(rew,[status(thm),theory(equality)],[23857,2604]),
[iquote('1:Rew:23857.0,2604.0')] ).
cnf(23883,plain,
equal(hAPP(hAPP(hAPP(c_Not,c_Not),c_Lattices_Oupper__semilattice__class_Osup(tc_fun(u,tc_bool))),v),v),
inference(rew,[status(thm),theory(equality)],[23857,44]),
[iquote('1:Rew:23857.0,44.0')] ).
cnf(25324,plain,
( ~ equal(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),c_Not)
| equal(hAPP(hAPP(c_Not,c_Not),c_Not),v) ),
inference(rew,[status(thm),theory(equality)],[23857,3741]),
[iquote('1:Rew:23857.0,3741.1')] ).
cnf(25544,plain,
equal(hAPP(hAPP(hAPP(c_Not,c_Not),c_Lattices_Olower__semilattice__class_Oinf(tc_fun(u,tc_bool))),v),c_HOL_Ominus__class_Ominus(v,w,tc_fun(u,tc_bool))),
inference(rew,[status(thm),theory(equality)],[23857,6879]),
[iquote('1:Rew:23857.0,6879.0')] ).
cnf(25680,plain,
equal(c_HOL_Ominus__class_Ominus(c_Set_Oinsert(hAPP(c_COMBC(hAPP(c_COMBC(hAPP(c_COMBB(c_Arrow__Order__Mirabelle_Obelow,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool),tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),tc_Arrow__Order__Mirabelle_Oindi),v_P____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),v_c____),tc_Arrow__Order__Mirabelle_Oindi,tc_Arrow__Order__Mirabelle_Oalt,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),v_b____),c_Arrow__Order__Mirabelle_OProf,tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))),hAPP(hAPP(c_Not,c_Not),c_fequal(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),tc_fun(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),tc_bool)),c_Arrow__Order__Mirabelle_OProf),
inference(rew,[status(thm),theory(equality)],[23857,834]),
[iquote('1:Rew:23857.0,834.0')] ).
cnf(25970,plain,
equal(hAPP(hAPP(hAPP(c_Not,c_Not),hAPP(c_Not,c_Not)),u),u),
inference(rew,[status(thm),theory(equality)],[23857,23883]),
[iquote('1:Rew:23857.0,23883.0')] ).
cnf(26449,plain,
~ equal(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),c_Not),
inference(aed,[status(thm),theory(equality)],[305,25324]),
[iquote('1:AED:305.0,25324.1')] ).
cnf(26474,plain,
equal(hAPP(hAPP(c_Not,c_Not),hAPP(c_Not,c_Not)),c_Set_Oinsert(u,v,w)),
inference(rew,[status(thm),theory(equality)],[23857,23874]),
[iquote('1:Rew:23857.0,23874.0')] ).
cnf(26475,plain,
equal(hAPP(hAPP(c_Not,c_Not),hAPP(c_Not,c_Not)),c_Arrow__Order__Mirabelle_OProf),
inference(rew,[status(thm),theory(equality)],[26474,1129]),
[iquote('1:Rew:26474.0,1129.0')] ).
cnf(26529,plain,
equal(hAPP(c_Arrow__Order__Mirabelle_OProf,u),u),
inference(rew,[status(thm),theory(equality)],[26475,25970]),
[iquote('1:Rew:26475.0,25970.0')] ).
cnf(26542,plain,
equal(c_Set_Oinsert(u,v,w),c_Arrow__Order__Mirabelle_OProf),
inference(rew,[status(thm),theory(equality)],[26475,26474]),
[iquote('1:Rew:26475.0,26474.0')] ).
cnf(26543,plain,
equal(v_P____,c_Not),
inference(rew,[status(thm),theory(equality)],[26529,20246]),
[iquote('1:Rew:26529.0,20246.0')] ).
cnf(26748,plain,
equal(hAPP(c_fequal(u),v),c_Arrow__Order__Mirabelle_OProf),
inference(rew,[status(thm),theory(equality)],[26542,1003]),
[iquote('1:Rew:26542.0,1003.0')] ).
cnf(26999,plain,
( ~ equal(hAPP(hAPP(c_fequal(u),v),w),c_Not)
| equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v),c_Not) ),
inference(rew,[status(thm),theory(equality)],[26748,21741]),
[iquote('1:Rew:26748.0,21741.1')] ).
cnf(27936,plain,
( ~ equal(u,c_Not)
| equal(v,c_Not) ),
inference(rew,[status(thm),theory(equality)],[26529,26999,26748]),
[iquote('1:Rew:26529.0,26999.1,26529.0,26999.0,26748.0,26999.0')] ).
cnf(27988,plain,
( ~ equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not)
| ~ equal(c_Not,c_Not)
| equal(u,w) ),
inference(rew,[status(thm),theory(equality)],[27936,21885]),
[iquote('1:Rew:27936.1,21885.1')] ).
cnf(28931,plain,
( ~ equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not)
| equal(u,w) ),
inference(obv,[status(thm),theory(equality)],[27988]),
[iquote('1:Obv:27988.1')] ).
cnf(28932,plain,
~ equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not),
inference(aed,[status(thm),theory(equality)],[305,28931]),
[iquote('1:AED:305.0,28931.1')] ).
cnf(29215,plain,
( equal(c_Set_Ovimage(u,c_Not,v,tc_bool),c_Not)
| equal(c_Set_Ovimage(u,c_Not,v,tc_bool),hAPP(c_Not,c_Not)) ),
inference(rew,[status(thm),theory(equality)],[700,22796]),
[iquote('1:Rew:700.0,22796.0')] ).
cnf(29216,plain,
equal(c_Set_Ovimage(u,c_Not,v,tc_bool),hAPP(c_Not,c_Not)),
inference(mrr,[status(thm)],[29215,28932]),
[iquote('1:MRR:29215.0,28932.0')] ).
cnf(29301,plain,
( equal(c_HOL_Ouminus__class_Ouminus(tc_fun(u,tc_bool)),c_Not)
| equal(hAPP(hAPP(c_Not,c_Not),v),hAPP(c_Not,c_Not)) ),
inference(rew,[status(thm),theory(equality)],[29216,23095]),
[iquote('1:Rew:29216.0,23095.1')] ).
cnf(29302,plain,
equal(hAPP(hAPP(c_Not,c_Not),u),hAPP(c_Not,c_Not)),
inference(mrr,[status(thm)],[29301,26449]),
[iquote('1:MRR:29301.0,26449.0')] ).
cnf(29505,plain,
equal(c_HOL_Ominus__class_Ominus(u,v,tc_fun(w,tc_bool)),hAPP(c_Not,c_Not)),
inference(rew,[status(thm),theory(equality)],[29302,25544]),
[iquote('1:Rew:29302.0,25544.0,29302.0,25544.0')] ).
cnf(31179,plain,
equal(hAPP(c_Not,c_Not),c_Arrow__Order__Mirabelle_OProf),
inference(rew,[status(thm),theory(equality)],[29505,25680,26542,26543,29302]),
[iquote('1:Rew:29505.0,25680.0,26542.0,25680.0,26543.0,25680.0,29302.0,25680.0')] ).
cnf(31180,plain,
$false,
inference(mrr,[status(thm)],[31179,23516]),
[iquote('1:MRR:31179.0,23516.0')] ).
cnf(31185,plain,
hBOOL(c_fequal(u)),
inference(spt,[spt(split,[position(s2)])],[14260]),
[iquote('1:Spt:31180.0,14260.1')] ).
cnf(31334,plain,
equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),c_fequal(u)),
inference(res,[status(thm),theory(equality)],[31185,19177]),
[iquote('1:Res:31185.0,19177.0')] ).
cnf(31351,plain,
~ hBOOL(hAPP(c_Not,c_fequal(u))),
inference(spl,[status(thm),theory(equality)],[31334,17403]),
[iquote('1:SpL:31334.0,17403.0')] ).
cnf(31392,plain,
( hBOOL(u)
| equal(hAPP(c_Not,c_fequal(v)),u) ),
inference(res,[status(thm),theory(equality)],[11521,31351]),
[iquote('1:Res:11521.0,31351.0')] ).
cnf(31457,plain,
( hBOOL(u)
| equal(hAPP(c_Not,u),c_fequal(v)) ),
inference(spr,[status(thm),theory(equality)],[31392,1913]),
[iquote('1:SpR:31392.1,1913.0')] ).
cnf(31663,plain,
( ~ equal(hAPP(c_Not,u),c_Not)
| hBOOL(u) ),
inference(spl,[status(thm),theory(equality)],[31457,5150]),
[iquote('1:SpL:31457.1,5150.0')] ).
cnf(31675,plain,
( ~ equal(u,c_Not)
| hBOOL(hAPP(c_Not,u)) ),
inference(spl,[status(thm),theory(equality)],[1913,31663]),
[iquote('1:SpL:1913.0,31663.0')] ).
cnf(31689,plain,
( ~ equal(u,c_Not)
| ~ hBOOL(u) ),
inference(res,[status(thm),theory(equality)],[31675,1716]),
[iquote('1:Res:31675.1,1716.1')] ).
cnf(31712,plain,
( ~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_fequal(v))
| ~ equal(w,c_Not)
| ~ hBOOL(x) ),
inference(mrr,[status(thm)],[12208,31689]),
[iquote('1:MRR:12208.3,31689.1')] ).
cnf(31720,plain,
( ~ equal(u,c_Not)
| hBOOL(c_Orderings_Obot__class_Obot(tc_fun(v,tc_bool))) ),
inference(mrr,[status(thm)],[14230,31689]),
[iquote('1:MRR:14230.2,31689.1')] ).
cnf(31742,plain,
hBOOL(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool))),
inference(aed,[status(thm),theory(equality)],[305,31720]),
[iquote('1:AED:305.0,31720.0')] ).
cnf(31802,plain,
( ~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_fequal(v))
| ~ hBOOL(w) ),
inference(aed,[status(thm),theory(equality)],[305,31712]),
[iquote('1:AED:305.0,31712.1')] ).
cnf(31804,plain,
( ~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_fequal(v))
| ~ equal(w,c_Arrow__Order__Mirabelle_OProf) ),
inference(mrr,[status(thm)],[11490,31802]),
[iquote('1:MRR:11490.2,31802.1')] ).
cnf(31807,plain,
~ equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),c_fequal(v)),
inference(aed,[status(thm),theory(equality)],[305,31804]),
[iquote('1:AED:305.0,31804.1')] ).
cnf(31830,plain,
equal(c_Orderings_Obot__class_Obot(tc_fun(u,tc_bool)),hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____)),
inference(res,[status(thm),theory(equality)],[31742,19177]),
[iquote('1:Res:31742.0,19177.0')] ).
cnf(32009,plain,
~ equal(hAPP(c_Arrow__Order__Mirabelle_OProf,v_P____),c_fequal(u)),
inference(rew,[status(thm),theory(equality)],[31830,31807]),
[iquote('1:Rew:31830.0,31807.0')] ).
cnf(32050,plain,
$false,
inference(unc,[status(thm)],[32009,31334]),
[iquote('1:UnC:32009.0,31334.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SCT043-1 : TPTP v8.1.0. Released v4.1.0.
% 0.10/0.11 % Command : run_spass %d %s
% 0.12/0.32 % Computer : n016.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Sat Jul 2 07:23:43 EDT 2022
% 0.12/0.32 % CPUTime :
% 32.74/32.90
% 32.74/32.90 SPASS V 3.9
% 32.74/32.90 SPASS beiseite: Proof found.
% 32.74/32.90 % SZS status Theorem
% 32.74/32.90 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.74/32.90 SPASS derived 25702 clauses, backtracked 6006 clauses, performed 3 splits and kept 17805 clauses.
% 32.74/32.90 SPASS allocated 107521 KBytes.
% 32.74/32.90 SPASS spent 0:0:32.55 on the problem.
% 32.74/32.90 0:00:00.06 for the input.
% 32.74/32.90 0:00:00.00 for the FLOTTER CNF translation.
% 32.74/32.90 0:00:00.22 for inferences.
% 32.74/32.90 0:00:00.60 for the backtracking.
% 32.74/32.90 0:0:31.33 for the reduction.
% 32.74/32.90
% 32.74/32.90
% 32.74/32.90 Here is a proof with depth 16, length 226 :
% 32.74/32.90 % SZS output start Refutation
% See solution above
% 32.74/32.91 Formulae used in the proof : cls_fun__upd__same_0 cls_fun__upd__idem_0 cls_Un__empty__left_0 cls_insert__is__Un_0 cls_Collect__neg__eq_0 cls_vimage__Collect__eq_0 cls_sup__commute_0 cls_Collect__def_0 cls_insert__not__empty_0 cls_insert__absorb2_0 cls_COMBK__def_0 cls_diff__eq_0 cls_Int__commute_0 cls_vimage__Compl_0 cls_Diff__insert__absorb_0 cls_double__complement_0 cls_double__compl_0 cls_bot1E_0 cls_compl__eq__compl__iff_0 cls_Compl__eq__Compl__iff_0 cls_vimage__const_1 cls_empty__not__insert_0 cls_Int__absorb_0 cls_singleton__conv_0 cls_vimage__code_0 cls_vimage__code_1 cls_singleton__conv2_0 cls_vimage__empty_0 cls_Collect__mem__eq_0 cls_ComplI_0 cls_ComplD_0 cls_insert__absorb_0 cls_mem__def_0 cls_CHAINED_0_01 clsarity_fun__Complete__Lattice_Ocomplete__lattice clsarity_fun__Lattices_Oupper__semilattice clsarity_fun__Lattices_Olower__semilattice clsarity_fun__Lattices_Odistrib__lattice clsarity_fun__Lattices_Obounded__lattice clsarity_fun__Lattices_Oboolean__algebra clsarity_fun__Orderings_Opreorder clsarity_fun__Lattices_Olattice clsarity_fun__Orderings_Oorder clsarity_fun__Orderings_Obot clsarity_fun__HOL_Oord clsarity_bool__Complete__Lattice_Ocomplete__lattice clsarity_bool__Lattices_Oupper__semilattice clsarity_bool__Lattices_Olower__semilattice clsarity_bool__Lattices_Odistrib__lattice clsarity_bool__Lattices_Obounded__lattice clsarity_bool__Lattices_Oboolean__algebra clsarity_bool__Finite__Set_Ofinite_Ofinite clsarity_bool__Orderings_Opreorder clsarity_bool__Lattices_Olattice clsarity_bool__Orderings_Oorder clsarity_bool__Orderings_Obot clsarity_bool__HOL_Oord cls_ATP__Linkup_OCOMBC__def_0 cls_ATP__Linkup_OCOMBB__def_0 cls_ATP__Linkup_Oequal__imp__fequal_0 cls_ATP__Linkup_Ofequal__imp__equal_0 cls_conjecture_0
% 33.23/33.46
%------------------------------------------------------------------------------