%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWV826-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 09:04:22 AM UTC 2026
% Result : Unsatisfiable 32.94s 38.24s
% Output : Proof 32.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_Diff__triv_0,axiom,
( c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)) = V_A
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Diff__triv_0) ).
cnf(cls_sup__fun__eq_0,axiom,
( hAPP(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(t_a,T_b)),V_f),V_g),v_x) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_b),hAPP(V_f,v_x)),hAPP(V_g,v_x))
| ~ class_Lattices_Olattice(T_b) ),
file('theBenchmark.p',cls_sup__fun__eq_0) ).
cnf(cls_inj__on__imageI_0,axiom,
( ~ c_Fun_Oinj__on(c_Fun_Ocomp(V_g,V_f,T_c,T_b,T_a),V_A,T_a,T_b)
| c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_c),T_c,T_b) ),
file('theBenchmark.p',cls_inj__on__imageI_0) ).
cnf(cls_Int__Un__distrib2_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)),V_A) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_A)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_C),V_A)),
file('theBenchmark.p',cls_Int__Un__distrib2_0) ).
cnf(cls_Int__Un__distrib_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_C)),
file('theBenchmark.p',cls_Int__Un__distrib_0) ).
cnf(cls_inf__sup__distrib1_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_z))
| ~ class_Lattices_Odistrib__lattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__distrib1_0) ).
cnf(cls_inf__sup__distrib2_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z)),V_x) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_x)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_z),V_x))
| ~ class_Lattices_Odistrib__lattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__distrib2_0) ).
cnf(cls_Int__Collect_1,axiom,
( ~ hBOOL(c_in(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),c_Collect(V_P,T_a)),T_a))
| hBOOL(hAPP(V_P,V_x)) ),
file('theBenchmark.p',cls_Int__Collect_1) ).
cnf(cls_Un__absorb_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_A) = V_A,
file('theBenchmark.p',cls_Un__absorb_0) ).
cnf(cls_sup__idem_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_x) = V_x
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__idem_0) ).
cnf(cls_inj__on__insert_2,axiom,
( ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),T_a,T_b),T_b))
| c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b) ),
file('theBenchmark.p',cls_inj__on__insert_2) ).
cnf(cls_INT__extend__simps_I4_J_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),V_B,T_b,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = V_A,
file('theBenchmark.p',cls_INT__extend__simps_I4_J_0) ).
cnf(cls_mem__def_1,axiom,
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(c_in(V_x,V_S,T_a)) ),
file('theBenchmark.p',cls_mem__def_1) ).
cnf(cls_mem__def_0,axiom,
( ~ hBOOL(c_in(V_x,V_S,T_a))
| hBOOL(hAPP(V_S,V_x)) ),
file('theBenchmark.p',cls_mem__def_0) ).
cnf(cls_COMBB__def_0,axiom,
hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)),
file('theBenchmark.p',cls_COMBB__def_0) ).
cnf(cls_COMBC__def_0,axiom,
c_COMBC(V_P,V_Q,V_R,T_b,T_c,T_a) = hAPP(hAPP(V_P,V_R),V_Q),
file('theBenchmark.p',cls_COMBC__def_0) ).
cnf(cls_COMBI__def_0,axiom,
hAPP(c_COMBI(T_a),V_P) = V_P,
file('theBenchmark.p',cls_COMBI__def_0) ).
cnf(cls_COMBK__def_0,axiom,
hAPP(c_COMBK(V_P,T_a,T_b),V_Q) = V_P,
file('theBenchmark.p',cls_COMBK__def_0) ).
cnf(cls_COMBS__def_0,axiom,
c_COMBS(V_P,V_Q,V_R,T_b,T_c,T_a) = hAPP(hAPP(V_P,V_R),hAPP(V_Q,V_R)),
file('theBenchmark.p',cls_COMBS__def_0) ).
cnf(cls_inj__on__Un_3,axiom,
( c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a,T_b)
| ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| ~ c_Fun_Oinj__on(V_f,V_B,T_a,T_b)
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_b,tc_bool)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a,T_b)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool)),T_a,T_b)) != c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_inj__on__Un_3) ).
cnf(cls_inj__on__Un_2,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a,T_b)
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_b,tc_bool)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a,T_b)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool)),T_a,T_b)) = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_inj__on__Un_2) ).
cnf(cls_Diff__idemp_0,axiom,
c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__idemp_0) ).
cnf(cls_eq__eqI_1,axiom,
( V_xa = V_y
| c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x,V_x,T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('theBenchmark.p',cls_eq__eqI_1) ).
cnf(cls_eq__eqI_0,axiom,
( V_x_H = V_y_H
| c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)
| ~ class_OrderedGroup_Oab__group__add(T_a) ),
file('theBenchmark.p',cls_eq__eqI_0) ).
cnf(cls_Max__mono_0,axiom,
( ~ c_lessequals(V_M,V_N,tc_fun(T_a,tc_bool))
| V_M = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_Finite__Set_Ofinite(V_N,T_a)
| c_lessequals(c_Finite__Set_Olinorder__class_OMax(V_M,T_a),c_Finite__Set_Olinorder__class_OMax(V_N,T_a),T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Max__mono_0) ).
cnf(cls_linorder_Oneq__iff_1,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('theBenchmark.p',cls_linorder_Oneq__iff_1) ).
cnf(cls_linorder_Onot__less__iff__gr__or__eq_2,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
file('theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_2) ).
cnf(cls_lessThan__subset__iff_1,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| c_lessequals(c_SetInterval_Oord__class_OlessThan(V_x,T_a),c_SetInterval_Oord__class_OlessThan(V_y,T_a),tc_fun(T_a,tc_bool))
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_lessThan__subset__iff_1) ).
cnf(cls_lessThan__subset__iff_0,axiom,
( ~ c_lessequals(c_SetInterval_Oord__class_OlessThan(V_x,T_a),c_SetInterval_Oord__class_OlessThan(V_y,T_a),tc_fun(T_a,tc_bool))
| c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_lessThan__subset__iff_0) ).
cnf(cls_image__diff__subset_0,axiom,
c_lessequals(c_HOL_Ominus__class_Ominus(c_Set_Oimage(V_f,V_A,T_b,T_a),c_Set_Oimage(V_f,V_B,T_b,T_a),tc_fun(T_a,tc_bool)),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_b,tc_bool)),T_b,T_a),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_image__diff__subset_0) ).
cnf(cls_Un__left__commute_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_C)),
file('theBenchmark.p',cls_Un__left__commute_0) ).
cnf(cls_Un__assoc_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)),V_C) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)),
file('theBenchmark.p',cls_Un__assoc_0) ).
cnf(cls_sup__assoc_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)),V_z) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z))
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__assoc_0) ).
cnf(cls_sup__left__commute_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_z))
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__left__commute_0) ).
cnf(cls_inf__sup__aci_I7_J_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_z))
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I7_J_0) ).
cnf(cls_inf__sup__aci_I6_J_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)),V_z) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z))
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I6_J_0) ).
cnf(cls_IntE_1,axiom,
( ~ hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),T_a))
| hBOOL(c_in(V_c,V_B,T_a)) ),
file('theBenchmark.p',cls_IntE_1) ).
cnf(cls_IntE_0,axiom,
( ~ hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),T_a))
| hBOOL(c_in(V_c,V_A,T_a)) ),
file('theBenchmark.p',cls_IntE_0) ).
cnf(cls_inj__on__contraD_0,axiom,
( ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| V_x = V_y
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_y,V_A,T_a))
| hAPP(V_f,V_x) != hAPP(V_f,V_y) ),
file('theBenchmark.p',cls_inj__on__contraD_0) ).
cnf(cls_inj__on__iff_0,axiom,
( V_x = V_y
| ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_y,V_A,T_a))
| hAPP(V_f,V_x) != hAPP(V_f,V_y) ),
file('theBenchmark.p',cls_inj__on__iff_0) ).
cnf(cls_inj__on__def_0,axiom,
( V_x = V_xa
| ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_xa,V_A,T_a))
| hAPP(V_f,V_x) != hAPP(V_f,V_xa) ),
file('theBenchmark.p',cls_inj__on__def_0) ).
cnf(cls_inj__onD_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_y,V_A,T_a))
| V_x = V_y
| ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| hAPP(V_f,V_x) != hAPP(V_f,V_y) ),
file('theBenchmark.p',cls_inj__onD_0) ).
cnf(cls_Int__absorb2_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) = V_A ),
file('theBenchmark.p',cls_Int__absorb2_0) ).
cnf(cls_Int__absorb1_0,axiom,
( ~ c_lessequals(V_B,V_A,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) = V_B ),
file('theBenchmark.p',cls_Int__absorb1_0) ).
cnf(cls_le__iff__inf_0,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y) = V_x
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__iff__inf_0) ).
cnf(cls_le__iff__inf_1,axiom,
( c_lessequals(V_x,V_y,T_a)
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y) != V_x
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__iff__inf_1) ).
cnf(cls_inf__absorb2_0,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y) = V_y
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__absorb2_0) ).
cnf(cls_Un__subset__iff_2,axiom,
( ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
| c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_C,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__subset__iff_2) ).
cnf(cls_Un__upper2_0,axiom,
c_lessequals(V_B,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Un__upper2_0) ).
cnf(cls_Un__upper1_0,axiom,
c_lessequals(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Un__upper1_0) ).
cnf(cls_Un__least_0,axiom,
( ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
| c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_C,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__least_0) ).
cnf(cls_le__supI_0,axiom,
( ~ c_lessequals(V_a,V_x,T_a)
| ~ c_lessequals(V_b,V_x,T_a)
| c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),V_b),V_x,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__supI_0) ).
cnf(cls_sup__ge1_0,axiom,
( c_lessequals(V_x,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__ge1_0) ).
cnf(cls_sup__ge2_0,axiom,
( c_lessequals(V_y,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__ge2_0) ).
cnf(cls_sup__least_0,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_lessequals(V_z,V_x,T_a)
| c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z),V_x,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__least_0) ).
cnf(cls_le__sup__iff_2,axiom,
( ~ c_lessequals(V_x,V_z,T_a)
| ~ c_lessequals(V_y,V_z,T_a)
| c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),V_z,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__sup__iff_2) ).
cnf(cls_inf__sup__ord_I4_J_0,axiom,
( c_lessequals(V_y,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),T_a)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__ord_I4_J_0) ).
cnf(cls_inf__sup__ord_I3_J_0,axiom,
( c_lessequals(V_x,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),T_a)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__ord_I3_J_0) ).
cnf(cls_Int__commute_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_A),
file('theBenchmark.p',cls_Int__commute_0) ).
cnf(cls_inf__commute_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_x)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__commute_0) ).
cnf(cls_inf__sup__aci_I1_J_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_x)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I1_J_0) ).
cnf(cls_Diff__partition_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool))) = V_B ),
file('theBenchmark.p',cls_Diff__partition_0) ).
cnf(cls_lessThan__eq__iff_0,axiom,
( V_x = V_y
| c_SetInterval_Oord__class_OlessThan(V_x,T_a) != c_SetInterval_Oord__class_OlessThan(V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_lessThan__eq__iff_0) ).
cnf(cls_com_Osimps_I14_J_0,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('theBenchmark.p',cls_com_Osimps_I14_J_0) ).
cnf(cls_distrib__inf__le_0,axiom,
( c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_z)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_z)),T_a)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_distrib__inf__le_0) ).
cnf(cls_Diff__subset_0,axiom,
c_lessequals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__subset_0) ).
cnf(cls_Un__Int__crazy_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C))),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_C),V_A)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C))),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_C),V_A)),
file('theBenchmark.p',cls_Un__Int__crazy_0) ).
cnf(cls_image__constant__conv_0,axiom,
c_Set_Oimage(c_COMBK(V_c,T_a,T_b),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_image__constant__conv_0) ).
cnf(cls_CollectI_0,axiom,
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
file('theBenchmark.p',cls_CollectI_0) ).
cnf(cls_CollectD_0,axiom,
( ~ hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a))
| hBOOL(hAPP(V_P,V_a)) ),
file('theBenchmark.p',cls_CollectD_0) ).
cnf(cls_image__constant_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| c_Set_Oimage(c_COMBK(V_c,T_b,T_a),V_A,T_a,T_b) = hAPP(hAPP(c_Set_Oinsert(T_b),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool))) ),
file('theBenchmark.p',cls_image__constant_0) ).
cnf(cls_image__subset__iff_0,axiom,
( ~ c_lessequals(c_Set_Oimage(V_f,V_A,T_b,T_a),V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_b))
| hBOOL(c_in(hAPP(V_f,V_x),V_B,T_a)) ),
file('theBenchmark.p',cls_image__subset__iff_0) ).
cnf(cls_finite__surj_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ c_lessequals(V_B,c_Set_Oimage(V_f,V_A,T_a,T_b),tc_fun(T_b,tc_bool))
| c_Finite__Set_Ofinite(V_B,T_b) ),
file('theBenchmark.p',cls_finite__surj_0) ).
cnf(cls_inj__on__image__Int_0,axiom,
( ~ c_Fun_Oinj__on(V_f,V_C,T_a,T_b)
| ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
| c_Set_Oimage(V_f,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),T_a,T_b) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_b,tc_bool)),c_Set_Oimage(V_f,V_A,T_a,T_b)),c_Set_Oimage(V_f,V_B,T_a,T_b)) ),
file('theBenchmark.p',cls_inj__on__image__Int_0) ).
cnf(cls_subset__insert__iff_0,axiom,
( ~ c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert__iff_0) ).
cnf(cls_subset__insert__iff_3,axiom,
( ~ c_lessequals(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert__iff_3) ).
cnf(cls_diff__single__insert_0,axiom,
( ~ c_lessequals(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_diff__single__insert_0) ).
cnf(cls_fold1__def_0,axiom,
c_Finite__Set_Ofold1(V_f,V_A,T_a) = c_The(c_Finite__Set_Ofold1Set(V_f,V_A,T_a),T_a),
file('theBenchmark.p',cls_fold1__def_0) ).
cnf(cls_le__SUPI_0,axiom,
( ~ hBOOL(c_in(V_i,V_A,T_a))
| c_lessequals(hAPP(V_M,V_i),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_M,T_a,T_b),T_b)
| ~ class_Complete__Lattice_Ocomplete__lattice(T_b) ),
file('theBenchmark.p',cls_le__SUPI_0) ).
cnf(cls_UN__upper_0,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_lessequals(hAPP(V_B,V_a),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_a,tc_fun(T_b,tc_bool)),tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_UN__upper_0) ).
cnf(cls_insert__Diff1_0,axiom,
( ~ hBOOL(c_in(V_x,V_B,T_a))
| c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),V_B,tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_insert__Diff1_0) ).
cnf(cls_image__ident_0,axiom,
c_Set_Oimage(c_COMBI(T_a),V_Y,T_a,T_a) = V_Y,
file('theBenchmark.p',cls_image__ident_0) ).
cnf(cls_com_Osimps_I17_J_0,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('theBenchmark.p',cls_com_Osimps_I17_J_0) ).
cnf(cls_below__fold1__iff_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_x,c_Finite__Set_Ofold1(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_A,T_a),T_a)
| ~ hBOOL(c_in(V_xa,V_A,T_a))
| c_lessequals(V_x,V_xa,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_below__fold1__iff_0) ).
cnf(cls_finite__Diff_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ),
file('theBenchmark.p',cls_finite__Diff_0) ).
cnf(cls_inj__on__diff_0,axiom,
( ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| c_Fun_Oinj__on(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a,T_b) ),
file('theBenchmark.p',cls_inj__on__diff_0) ).
cnf(cls_Inf__insert_0,axiom,
( c_Complete__Lattice_OInf__class_OInf(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),c_Complete__Lattice_OInf__class_OInf(V_A,T_a))
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Inf__insert_0) ).
cnf(cls_Collect__def_0,axiom,
c_Collect(V_P,T_a) = V_P,
file('theBenchmark.p',cls_Collect__def_0) ).
cnf(cls_fun__left__comm__idem__sup_0,axiom,
( c_Finite__Set_Ofun__left__comm__idem(c_Lattices_Oupper__semilattice__class_Osup(T_a),T_a,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_fun__left__comm__idem__sup_0) ).
cnf(cls_com_Osimps_I3_J_1,axiom,
( V_com2 = V_com2_H
| c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) ),
file('theBenchmark.p',cls_com_Osimps_I3_J_1) ).
cnf(cls_com_Osimps_I3_J_0,axiom,
( V_com1 = V_com1_H
| c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) ),
file('theBenchmark.p',cls_com_Osimps_I3_J_0) ).
cnf(cls_com_Osimps_I46_J_0,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('theBenchmark.p',cls_com_Osimps_I46_J_0) ).
cnf(cls_Sup__insert_0,axiom,
( c_Complete__Lattice_OSup__class_OSup(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),c_Complete__Lattice_OSup__class_OSup(V_A,T_a))
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Sup__insert_0) ).
cnf(cls_com_Osimps_I44_J_0,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('theBenchmark.p',cls_com_Osimps_I44_J_0) ).
cnf(cls_finite__Diff2_0,axiom,
( ~ c_Finite__Set_Ofinite(V_B,T_a)
| ~ c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| c_Finite__Set_Ofinite(V_A,T_a) ),
file('theBenchmark.p',cls_finite__Diff2_0) ).
cnf(cls_finite__Diff2_1,axiom,
( ~ c_Finite__Set_Ofinite(V_B,T_a)
| ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ),
file('theBenchmark.p',cls_finite__Diff2_1) ).
cnf(cls_inj__on__id2_0,axiom,
c_Fun_Oinj__on(c_COMBI(T_a),V_A,T_a,T_a),
file('theBenchmark.p',cls_inj__on__id2_0) ).
cnf(cls_finite__UN_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ c_Finite__Set_Ofinite(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_a,tc_fun(T_b,tc_bool)),T_b)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| c_Finite__Set_Ofinite(hAPP(V_B,V_x),T_b) ),
file('theBenchmark.p',cls_finite__UN_0) ).
cnf(cls_UNION__empty__conv_I2_J_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_b))
| hAPP(V_B,V_x) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_b,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_UNION__empty__conv_I2_J_0) ).
cnf(cls_com_Osimps_I52_J_0,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('theBenchmark.p',cls_com_Osimps_I52_J_0) ).
cnf(cls_DiffE_0,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| hBOOL(c_in(V_c,V_A,T_a)) ),
file('theBenchmark.p',cls_DiffE_0) ).
cnf(cls_inj__on__Un__image__eq__iff_0,axiom,
( V_A = V_B
| ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a,T_b)
| c_Set_Oimage(V_f,V_A,T_a,T_b) != c_Set_Oimage(V_f,V_B,T_a,T_b) ),
file('theBenchmark.p',cls_inj__on__Un__image__eq__iff_0) ).
cnf(cls_DiffE_1,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
file('theBenchmark.p',cls_DiffE_1) ).
cnf(cls_UN__subset__iff_0,axiom,
( ~ c_lessequals(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_I,V_A,T_b,tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_I,T_b))
| c_lessequals(hAPP(V_A,V_x),V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_UN__subset__iff_0) ).
cnf(cls_K__record__comp_0,axiom,
hAPP(c_Fun_Ocomp(c_COMBK(V_c,T_b,T_c),V_f,T_c,T_b,t_a),v_x) = V_c,
file('theBenchmark.p',cls_K__record__comp_0) ).
cnf(cls_com_Osimps_I45_J_0,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('theBenchmark.p',cls_com_Osimps_I45_J_0) ).
cnf(cls_UN__absorb_0,axiom,
( ~ hBOOL(c_in(V_k,V_I,T_a))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_b,tc_bool)),hAPP(V_A,V_k)),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_I,V_A,T_a,tc_fun(T_b,tc_bool))) = c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_I,V_A,T_a,tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_UN__absorb_0) ).
cnf(cls_com_Osimps_I4_J_2,axiom,
( V_com2 = V_com2_H
| c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) ),
file('theBenchmark.p',cls_com_Osimps_I4_J_2) ).
cnf(cls_com_Osimps_I4_J_1,axiom,
( V_com1 = V_com1_H
| c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) ),
file('theBenchmark.p',cls_com_Osimps_I4_J_1) ).
cnf(cls_com_Osimps_I4_J_0,axiom,
( V_fun = V_fun_H
| c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) ),
file('theBenchmark.p',cls_com_Osimps_I4_J_0) ).
cnf(cls_image__Int__subset_0,axiom,
c_lessequals(c_Set_Oimage(V_f,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_b,tc_bool)),V_A),V_B),T_b,T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),c_Set_Oimage(V_f,V_A,T_b,T_a)),c_Set_Oimage(V_f,V_B,T_b,T_a)),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_image__Int__subset_0) ).
cnf(cls_finite__Un_2,axiom,
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| ~ c_Finite__Set_Ofinite(V_G,T_a)
| c_Finite__Set_Ofinite(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_F),V_G),T_a) ),
file('theBenchmark.p',cls_finite__Un_2) ).
cnf(cls_finite__UnI_0,axiom,
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| ~ c_Finite__Set_Ofinite(V_G,T_a)
| c_Finite__Set_Ofinite(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_F),V_G),T_a) ),
file('theBenchmark.p',cls_finite__UnI_0) ).
cnf(cls_atLeastatMost__subset__iff_3,axiom,
( ~ c_lessequals(V_c,V_a,T_a)
| ~ c_lessequals(V_b,V_d,T_a)
| c_lessequals(c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a),c_SetInterval_Oord__class_OatLeastAtMost(V_c,V_d,T_a),tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__subset__iff_3) ).
cnf(cls_atLeastatMost__subset__iff_1,axiom,
( ~ c_lessequals(c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a),c_SetInterval_Oord__class_OatLeastAtMost(V_c,V_d,T_a),tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_a,V_b,T_a)
| c_lessequals(V_b,V_d,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__subset__iff_1) ).
cnf(cls_atLeastatMost__subset__iff_0,axiom,
( ~ c_lessequals(c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a),c_SetInterval_Oord__class_OatLeastAtMost(V_c,V_d,T_a),tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_a,V_b,T_a)
| c_lessequals(V_c,V_a,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__subset__iff_0) ).
cnf(cls_Un__Int__assoc__eq_0,axiom,
( c_lessequals(V_C,V_A,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)),V_C) != hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)) ),
file('theBenchmark.p',cls_Un__Int__assoc__eq_0) ).
cnf(cls_Un__Int__assoc__eq_1,axiom,
( ~ c_lessequals(V_C,V_A,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)),V_C) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)) ),
file('theBenchmark.p',cls_Un__Int__assoc__eq_1) ).
cnf(cls_o__apply_0,axiom,
hAPP(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),V_x) = hAPP(V_f,hAPP(V_g,V_x)),
file('theBenchmark.p',cls_o__apply_0) ).
cnf(cls_o__eq__dest__lhs_0,axiom,
hAPP(V_a,hAPP(V_b,V_v)) = hAPP(c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a),V_v),
file('theBenchmark.p',cls_o__eq__dest__lhs_0) ).
cnf(cls_atLeastatMost__subset__iff_2,axiom,
( c_lessequals(V_a,V_b,T_a)
| c_lessequals(c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a),c_SetInterval_Oord__class_OatLeastAtMost(V_c,V_d,T_a),tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__subset__iff_2) ).
cnf(cls_sup1E_0,axiom,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_x))
| hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(V_B,V_x)) ),
file('theBenchmark.p',cls_sup1E_0) ).
cnf(cls_sup1CI_0,axiom,
( ~ hBOOL(hAPP(V_B,V_x))
| hBOOL(hAPP(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_x)) ),
file('theBenchmark.p',cls_sup1CI_0) ).
cnf(cls_sup1CI_1,axiom,
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_x)) ),
file('theBenchmark.p',cls_sup1CI_1) ).
cnf(cls_endo__inj__surj_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ c_lessequals(c_Set_Oimage(V_f,V_A,T_a,T_a),V_A,tc_fun(T_a,tc_bool))
| ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_a)
| c_Set_Oimage(V_f,V_A,T_a,T_a) = V_A ),
file('theBenchmark.p',cls_endo__inj__surj_0) ).
cnf(cls_UnE_0,axiom,
( ~ hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a))
| hBOOL(c_in(V_c,V_A,T_a))
| hBOOL(c_in(V_c,V_B,T_a)) ),
file('theBenchmark.p',cls_UnE_0) ).
cnf(cls_inf__sup__aci_I2_J_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)),V_z) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z))
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I2_J_0) ).
cnf(cls_inf__sup__aci_I3_J_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_z))
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I3_J_0) ).
cnf(cls_inf__left__commute_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_z))
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__left__commute_0) ).
cnf(cls_inf__assoc_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)),V_z) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z))
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__assoc_0) ).
cnf(cls_Int__assoc_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)),V_C) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C)),
file('theBenchmark.p',cls_Int__assoc_0) ).
cnf(cls_Int__left__commute_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_C)),
file('theBenchmark.p',cls_Int__left__commute_0) ).
cnf(cls_UNION__empty__conv_I1_J_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_b))
| hAPP(V_B,V_x) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_b,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_UNION__empty__conv_I1_J_0) ).
cnf(cls_finite__Un_0,axiom,
( ~ c_Finite__Set_Ofinite(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_F),V_G),T_a)
| c_Finite__Set_Ofinite(V_F,T_a) ),
file('theBenchmark.p',cls_finite__Un_0) ).
cnf(cls_finite__Un_1,axiom,
( ~ c_Finite__Set_Ofinite(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_F),V_G),T_a)
| c_Finite__Set_Ofinite(V_G,T_a) ),
file('theBenchmark.p',cls_finite__Un_1) ).
cnf(cls_UN__extend__simps_I2_J_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),V_A,T_b,tc_fun(T_a,tc_bool))),V_B) = V_B,
file('theBenchmark.p',cls_UN__extend__simps_I2_J_0) ).
cnf(cls_UN__extend__simps_I3_J_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),V_B,T_b,tc_fun(T_a,tc_bool))) = V_A,
file('theBenchmark.p',cls_UN__extend__simps_I3_J_0) ).
cnf(cls_com_Osimps_I16_J_0,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('theBenchmark.p',cls_com_Osimps_I16_J_0) ).
cnf(cls_Diff__Int__distrib_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_C),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))) = c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_C),V_A),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_C),V_B),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__Int__distrib_0) ).
cnf(cls_Diff__Int__distrib2_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))),V_C) = c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_C),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__Int__distrib2_0) ).
cnf(cls_Diff__mono_0,axiom,
( ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_D,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_C,V_D,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Diff__mono_0) ).
cnf(cls_disjoint__iff__not__equal_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
file('theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
cnf(cls_distrib__sup__le_0,axiom,
( c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_z)),T_a)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_distrib__sup__le_0) ).
cnf(cls_Diff__Int2_0,axiom,
c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_C),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C),tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_C),V_B,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__Int2_0) ).
cnf(cls_sup__inf__absorb_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)) = V_x
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_sup__inf__absorb_0) ).
cnf(cls_equalityI_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_A,tc_fun(T_a,tc_bool))
| V_A = V_B ),
file('theBenchmark.p',cls_equalityI_0) ).
cnf(cls_set__eq__subset_2,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_A,tc_fun(T_a,tc_bool))
| V_A = V_B ),
file('theBenchmark.p',cls_set__eq__subset_2) ).
cnf(cls_order__eq__iff_2,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| V_x = V_y
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_order__eq__iff_2) ).
cnf(cls_order__antisym_0,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| V_x = V_y
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_order__antisym_0) ).
cnf(cls_order__antisym__conv_0,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| V_x = V_y
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_order__antisym__conv_0) ).
cnf(cls_inf__sup__absorb_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)) = V_x
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__absorb_0) ).
cnf(cls_Un__Diff__Int_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)) = V_A,
file('theBenchmark.p',cls_Un__Diff__Int_0) ).
cnf(cls_sup__absorb1_0,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y) = V_x
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__absorb1_0) ).
cnf(cls_le__iff__sup_1,axiom,
( c_lessequals(V_x,V_y,T_a)
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y) != V_y
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__iff__sup_1) ).
cnf(cls_le__iff__sup_0,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y) = V_y
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__iff__sup_0) ).
cnf(cls_Un__absorb1_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) = V_B ),
file('theBenchmark.p',cls_Un__absorb1_0) ).
cnf(cls_Un__absorb2_0,axiom,
( ~ c_lessequals(V_B,V_A,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) = V_A ),
file('theBenchmark.p',cls_Un__absorb2_0) ).
cnf(cls_subset__Un__eq_1,axiom,
( c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) != V_B ),
file('theBenchmark.p',cls_subset__Un__eq_1) ).
cnf(cls_finite__imageI_0,axiom,
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
file('theBenchmark.p',cls_finite__imageI_0) ).
cnf(cls_bot__empty__eq_0,axiom,
hAPP(c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),v_x) = c_in(v_x,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),
file('theBenchmark.p',cls_bot__empty__eq_0) ).
cnf(cls_Min__antimono_0,axiom,
( ~ c_lessequals(V_M,V_N,tc_fun(T_a,tc_bool))
| V_M = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_Finite__Set_Ofinite(V_N,T_a)
| c_lessequals(c_Finite__Set_Olinorder__class_OMin(V_N,T_a),c_Finite__Set_Olinorder__class_OMin(V_M,T_a),T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Min__antimono_0) ).
cnf(cls_linorder_Onot__less__iff__gr__or__eq_1,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_1) ).
cnf(cls_linorder_OleD_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('theBenchmark.p',cls_linorder_OleD_0) ).
cnf(cls_linorder_OleI_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x)) ),
file('theBenchmark.p',cls_linorder_OleI_0) ).
cnf(cls_linorder_Olinear_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y))
| hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x)) ),
file('theBenchmark.p',cls_linorder_Olinear_0) ).
cnf(cls_linorder_Onot__le_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y))
| hBOOL(hAPP(hAPP(V_less,V_y),V_x)) ),
file('theBenchmark.p',cls_linorder_Onot__le_0) ).
cnf(cls_linorder_Onot__le_1,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
file('theBenchmark.p',cls_linorder_Onot__le_1) ).
cnf(cls_linorder_Onot__leE_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('theBenchmark.p',cls_linorder_Onot__leE_0) ).
cnf(cls_linorder_Oantisym__conv1_1,axiom,
( hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('theBenchmark.p',cls_linorder_Oantisym__conv1_1) ).
cnf(cls_linorder_Oantisym__conv2_1,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
file('theBenchmark.p',cls_linorder_Oantisym__conv2_1) ).
cnf(cls_Diff__iff_2,axiom,
( ~ hBOOL(c_in(V_c,V_A,T_a))
| hBOOL(c_in(V_c,V_B,T_a))
| hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)) ),
file('theBenchmark.p',cls_Diff__iff_2) ).
cnf(cls_DiffI_0,axiom,
( ~ hBOOL(c_in(V_c,V_A,T_a))
| hBOOL(c_in(V_c,V_B,T_a))
| hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)) ),
file('theBenchmark.p',cls_DiffI_0) ).
cnf(cls_insert__subset_0,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),V_B,tc_fun(T_a,tc_bool))
| hBOOL(c_in(V_x,V_B,T_a)) ),
file('theBenchmark.p',cls_insert__subset_0) ).
cnf(cls_SUP__const_0,axiom,
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,c_COMBK(V_M,T_b,T_a),T_a,T_b) = V_M
| ~ class_Complete__Lattice_Ocomplete__lattice(T_b) ),
file('theBenchmark.p',cls_SUP__const_0) ).
cnf(cls_insert__image_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| hAPP(hAPP(c_Set_Oinsert(T_b),hAPP(V_f,V_x)),c_Set_Oimage(V_f,V_A,T_a,T_b)) = c_Set_Oimage(V_f,V_A,T_a,T_b) ),
file('theBenchmark.p',cls_insert__image_0) ).
cnf(cls_subset__insert__iff_2,axiom,
( hBOOL(c_in(V_x,V_A,T_a))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert__iff_2) ).
cnf(cls_subset__insert__iff_1,axiom,
( ~ c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool))
| hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert__iff_1) ).
cnf(cls_subset__insert_1,axiom,
( hBOOL(c_in(V_x,V_A,T_a))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert_1) ).
cnf(cls_subset__insert_0,axiom,
( hBOOL(c_in(V_x,V_A,T_a))
| ~ c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool))
| c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert_0) ).
cnf(cls_Int__insert__right_1,axiom,
( hBOOL(c_in(V_a,V_A,T_a))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) ),
file('theBenchmark.p',cls_Int__insert__right_1) ).
cnf(cls_Int__insert__left_1,axiom,
( hBOOL(c_in(V_a,V_C,T_a))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)),V_C) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C) ),
file('theBenchmark.p',cls_Int__insert__left_1) ).
cnf(cls_UN__iff_2,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_b))
| ~ hBOOL(c_in(V_b,hAPP(V_B,V_x),T_a))
| hBOOL(c_in(V_b,c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_b,tc_fun(T_a,tc_bool)),T_a)) ),
file('theBenchmark.p',cls_UN__iff_2) ).
cnf(cls_UN__I_0,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| ~ hBOOL(c_in(V_b,hAPP(V_B,V_a),T_b))
| hBOOL(c_in(V_b,c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_a,tc_fun(T_b,tc_bool)),T_b)) ),
file('theBenchmark.p',cls_UN__I_0) ).
cnf(cls_Un__Diff__cancel2_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool))),V_A) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_A),
file('theBenchmark.p',cls_Un__Diff__cancel2_0) ).
cnf(cls_Un__Diff__cancel_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool))) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),
file('theBenchmark.p',cls_Un__Diff__cancel_0) ).
cnf(cls_fun__diff__def_0,axiom,
( hAPP(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(t_a,T_b)),v_x) = c_HOL_Ominus__class_Ominus(hAPP(V_A,v_x),hAPP(V_B,v_x),T_b)
| ~ class_HOL_Ominus(T_b) ),
file('theBenchmark.p',cls_fun__diff__def_0) ).
cnf(cls_Int__subset__iff_1,axiom,
( ~ c_lessequals(V_C,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool))
| c_lessequals(V_C,V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Int__subset__iff_1) ).
cnf(cls_Int__subset__iff_0,axiom,
( ~ c_lessequals(V_C,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool))
| c_lessequals(V_C,V_A,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Int__subset__iff_0) ).
cnf(cls_le__infE_0,axiom,
( ~ c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),V_b),T_a)
| c_lessequals(V_x,V_a,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__infE_0) ).
cnf(cls_le__infE_1,axiom,
( ~ c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),V_b),T_a)
| c_lessequals(V_x,V_b,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__infE_1) ).
cnf(cls_le__infI1_0,axiom,
( ~ c_lessequals(V_a,V_x,T_a)
| c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),V_b),V_x,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__infI1_0) ).
cnf(cls_le__infI2_0,axiom,
( ~ c_lessequals(V_b,V_x,T_a)
| c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),V_b),V_x,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__infI2_0) ).
cnf(cls_le__inf__iff_0,axiom,
( ~ c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z),T_a)
| c_lessequals(V_x,V_y,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__inf__iff_0) ).
cnf(cls_le__inf__iff_1,axiom,
( ~ c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z),T_a)
| c_lessequals(V_x,V_z,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__inf__iff_1) ).
cnf(cls_Un__Diff_0,axiom,
c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_C,tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_A,V_C,tc_fun(T_a,tc_bool))),c_HOL_Ominus__class_Ominus(V_B,V_C,tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_Un__Diff_0) ).
cnf(cls_complete__lattice_OInf__lower_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| hBOOL(hAPP(hAPP(V_less__eq,hAPP(V_Inf,V_A)),V_x)) ),
file('theBenchmark.p',cls_complete__lattice_OInf__lower_0) ).
cnf(cls_complete__lattice_OSup__upper_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| hBOOL(hAPP(hAPP(V_less__eq,V_x),hAPP(V_Sup,V_A))) ),
file('theBenchmark.p',cls_complete__lattice_OSup__upper_0) ).
cnf(cls_Un__commute_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_A),
file('theBenchmark.p',cls_Un__commute_0) ).
cnf(cls_sup__commute_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_x)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__commute_0) ).
cnf(cls_inf__sup__aci_I5_J_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_x)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I5_J_0) ).
cnf(cls_com_Osimps_I5_J_0,axiom,
( V_fun = V_fun_H
| c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H) ),
file('theBenchmark.p',cls_com_Osimps_I5_J_0) ).
cnf(cls_com_Osimps_I5_J_1,axiom,
( V_com = V_com_H
| c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OWhile(V_fun_H,V_com_H) ),
file('theBenchmark.p',cls_com_Osimps_I5_J_1) ).
cnf(cls_Un__left__absorb_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),
file('theBenchmark.p',cls_Un__left__absorb_0) ).
cnf(cls_sup__left__idem_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_sup__left__idem_0) ).
cnf(cls_inf__sup__aci_I8_J_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I8_J_0) ).
cnf(cls_comp__inj__on_0,axiom,
( ~ c_Fun_Oinj__on(V_f,V_A,T_a,T_b)
| ~ c_Fun_Oinj__on(V_g,c_Set_Oimage(V_f,V_A,T_a,T_b),T_b,T_c)
| c_Fun_Oinj__on(c_Fun_Ocomp(V_g,V_f,T_b,T_c,T_a),V_A,T_a,T_c) ),
file('theBenchmark.p',cls_comp__inj__on_0) ).
cnf(cls_com_Osimps_I15_J_0,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('theBenchmark.p',cls_com_Osimps_I15_J_0) ).
cnf(cls_SUP1__iff_2,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(hAPP(hAPP(V_B,V_x),V_b))
| hBOOL(hAPP(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_a,tc_fun(T_b,tc_bool)),V_b)) ),
file('theBenchmark.p',cls_SUP1__iff_2) ).
cnf(cls_SUP1__I_0,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| ~ hBOOL(hAPP(hAPP(V_B,V_a),V_b))
| hBOOL(hAPP(c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_a,tc_fun(T_b,tc_bool)),V_b)) ),
file('theBenchmark.p',cls_SUP1__I_0) ).
cnf(cls_Diff__disjoint_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),c_HOL_Ominus__class_Ominus(V_B,V_A,tc_fun(T_a,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__disjoint_0) ).
cnf(cls_com_Osimps_I53_J_0,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('theBenchmark.p',cls_com_Osimps_I53_J_0) ).
cnf(cls_finite_0,axiom,
( c_Finite__Set_Ofinite(V_A,T_a)
| ~ class_Finite__Set_Ofinite_Ofinite(T_a) ),
file('theBenchmark.p',cls_finite_0) ).
cnf(cls_Int__Collect_0,axiom,
( ~ hBOOL(c_in(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),c_Collect(V_P,T_a)),T_a))
| hBOOL(c_in(V_x,V_A,T_a)) ),
file('theBenchmark.p',cls_Int__Collect_0) ).
cnf(cls_inj__on__insert_1,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),T_a,T_b),T_b)) ),
file('theBenchmark.p',cls_inj__on__insert_1) ).
cnf(cls_linorder_Oantisym__conv2_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y))
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| V_x = V_y ),
file('theBenchmark.p',cls_linorder_Oantisym__conv2_0) ).
cnf(cls_linorder_Oantisym__conv1_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y))
| V_x = V_y ),
file('theBenchmark.p',cls_linorder_Oantisym__conv1_0) ).
cnf(cls_insert__Diff__if_1,axiom,
( hBOOL(c_in(V_x,V_B,T_a))
| c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),V_B,tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))) ),
file('theBenchmark.p',cls_insert__Diff__if_1) ).
cnf(cls_inf1E_1,axiom,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),V_x))
| hBOOL(hAPP(V_B,V_x)) ),
file('theBenchmark.p',cls_inf1E_1) ).
cnf(cls_inf1E_0,axiom,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),V_x))
| hBOOL(hAPP(V_A,V_x)) ),
file('theBenchmark.p',cls_inf1E_0) ).
cnf(cls_finite__surj__inj_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ c_lessequals(V_A,c_Set_Oimage(V_f,V_A,T_a,T_a),tc_fun(T_a,tc_bool))
| c_Fun_Oinj__on(V_f,V_A,T_a,T_a) ),
file('theBenchmark.p',cls_finite__surj__inj_0) ).
cnf(cls_inj__on__Un_1,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a,T_b)
| c_Fun_Oinj__on(V_f,V_B,T_a,T_b) ),
file('theBenchmark.p',cls_inj__on__Un_1) ).
cnf(cls_inj__on__Un_0,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a,T_b)
| c_Fun_Oinj__on(V_f,V_A,T_a,T_b) ),
file('theBenchmark.p',cls_inj__on__Un_0) ).
cnf(cls_rev__image__eqI_0,axiom,
( hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_aa)) ),
file('theBenchmark.p',cls_rev__image__eqI_0) ).
cnf(cls_image__iff_2,axiom,
( hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a))
| ~ hBOOL(c_in(V_x,V_A,T_b)) ),
file('theBenchmark.p',cls_image__iff_2) ).
cnf(cls_image__eqI_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_b))
| hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)) ),
file('theBenchmark.p',cls_image__eqI_0) ).
cnf(cls_imageI_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| hBOOL(c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_a,T_b),T_b)) ),
file('theBenchmark.p',cls_imageI_0) ).
cnf(cls_Diff__subset__conv_1,axiom,
( ~ c_lessequals(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C),tc_fun(T_a,tc_bool))
| c_lessequals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Diff__subset__conv_1) ).
cnf(cls_Diff__subset__conv_0,axiom,
( ~ c_lessequals(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Diff__subset__conv_0) ).
cnf(cls_fun__left__comm__idem__inf_0,axiom,
( c_Finite__Set_Ofun__left__comm__idem(c_Lattices_Olower__semilattice__class_Oinf(T_a),T_a,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_fun__left__comm__idem__inf_0) ).
cnf(cls_finite__Int_1,axiom,
( ~ c_Finite__Set_Ofinite(V_G,T_a)
| c_Finite__Set_Ofinite(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_F),V_G),T_a) ),
file('theBenchmark.p',cls_finite__Int_1) ).
cnf(cls_finite__Int_0,axiom,
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_F),V_G),T_a) ),
file('theBenchmark.p',cls_finite__Int_0) ).
cnf(cls_le__funD_0,axiom,
( ~ c_lessequals(V_f,V_g,tc_fun(T_a,T_b))
| c_lessequals(hAPP(V_f,V_x),hAPP(V_g,V_x),T_b)
| ~ class_HOL_Oord(T_b) ),
file('theBenchmark.p',cls_le__funD_0) ).
cnf(cls_sup__bot__left_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),c_Orderings_Obot__class_Obot(T_a)),V_x) = V_x
| ~ class_Lattices_Obounded__lattice(T_a) ),
file('theBenchmark.p',cls_sup__bot__left_0) ).
cnf(cls_sup__bot__right_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),c_Orderings_Obot__class_Obot(T_a)) = V_x
| ~ class_Lattices_Obounded__lattice(T_a) ),
file('theBenchmark.p',cls_sup__bot__right_0) ).
cnf(cls_inf__bot__left_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),c_Orderings_Obot__class_Obot(T_a)),V_x) = c_Orderings_Obot__class_Obot(T_a)
| ~ class_Lattices_Obounded__lattice(T_a) ),
file('theBenchmark.p',cls_inf__bot__left_0) ).
cnf(cls_inf__bot__right_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),c_Orderings_Obot__class_Obot(T_a)) = c_Orderings_Obot__class_Obot(T_a)
| ~ class_Lattices_Obounded__lattice(T_a) ),
file('theBenchmark.p',cls_inf__bot__right_0) ).
cnf(cls_bot__least_0,axiom,
( c_lessequals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a)
| ~ class_Orderings_Obot(T_a) ),
file('theBenchmark.p',cls_bot__least_0) ).
cnf(cls_sup__eq__bot__eq1_0,axiom,
( V_A = c_Orderings_Obot__class_Obot(T_a)
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_A),V_B) != c_Orderings_Obot__class_Obot(T_a)
| ~ class_Lattices_Obounded__lattice(T_a) ),
file('theBenchmark.p',cls_sup__eq__bot__eq1_0) ).
cnf(cls_sup__eq__bot__eq2_0,axiom,
( V_B = c_Orderings_Obot__class_Obot(T_a)
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_A),V_B) != c_Orderings_Obot__class_Obot(T_a)
| ~ class_Lattices_Obounded__lattice(T_a) ),
file('theBenchmark.p',cls_sup__eq__bot__eq2_0) ).
cnf(cls_Un__empty_2,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Un__empty_2) ).
cnf(cls_image__is__empty_0,axiom,
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool))
| c_Set_Oimage(V_f,V_A,T_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_image__is__empty_0) ).
cnf(cls_complete__lattice_OInf__empty_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Inf,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) = V_top ),
file('theBenchmark.p',cls_complete__lattice_OInf__empty_0) ).
cnf(cls_complete__lattice_OSup__empty_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Sup,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) = V_bot ),
file('theBenchmark.p',cls_complete__lattice_OSup__empty_0) ).
cnf(cls_empty__Collect__eq_0,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
file('theBenchmark.p',cls_empty__Collect__eq_0) ).
cnf(cls_ex__in__conv_0,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('theBenchmark.p',cls_ex__in__conv_0) ).
cnf(cls_ball__empty_0,axiom,
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| hBOOL(hAPP(V_P,V_x)) ),
file('theBenchmark.p',cls_ball__empty_0) ).
cnf(cls_empty__iff_0,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('theBenchmark.p',cls_empty__iff_0) ).
cnf(cls_emptyE_0,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('theBenchmark.p',cls_emptyE_0) ).
cnf(cls_subset__empty_1,axiom,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_subset__empty_1) ).
cnf(cls_subset__empty_0,axiom,
( ~ c_lessequals(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool))
| V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__empty_0) ).
cnf(cls_Collect__empty__eq_0,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Collect__empty__eq_0) ).
cnf(cls_empty__fold1SetE_0,axiom,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
file('theBenchmark.p',cls_empty__fold1SetE_0) ).
cnf(cls_empty__Diff_0,axiom,
c_HOL_Ominus__class_Ominus(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_empty__Diff_0) ).
cnf(cls_Un__empty__right_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) = V_A,
file('theBenchmark.p',cls_Un__empty__right_0) ).
cnf(cls_Un__empty__left_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),V_B) = V_B,
file('theBenchmark.p',cls_Un__empty__left_0) ).
cnf(cls_Diff__cancel_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,V_A,tc_fun(T_a,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__cancel_0) ).
cnf(cls_Diff__empty_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = V_A,
file('theBenchmark.p',cls_Diff__empty_0) ).
cnf(cls_finite_OemptyI_0,axiom,
c_Finite__Set_Ofinite(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('theBenchmark.p',cls_finite_OemptyI_0) ).
cnf(cls_Int__empty__right_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Int__empty__right_0) ).
cnf(cls_Int__empty__left_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),V_B) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Int__empty__left_0) ).
cnf(cls_empty__subsetI_0,axiom,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_empty__subsetI_0) ).
cnf(cls_empty__is__image_0,axiom,
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oimage(V_f,V_A,T_b,T_a) ),
file('theBenchmark.p',cls_empty__is__image_0) ).
cnf(cls_image__empty_0,axiom,
c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_image__empty_0) ).
cnf(cls_inj__on__empty_0,axiom,
c_Fun_Oinj__on(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a,T_b),
file('theBenchmark.p',cls_inj__on__empty_0) ).
cnf(cls_bex__empty_0,axiom,
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('theBenchmark.p',cls_bex__empty_0) ).
cnf(cls_Un__empty_1,axiom,
( V_B = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__empty_1) ).
cnf(cls_Un__empty_0,axiom,
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__empty_0) ).
cnf(cls_empty__is__image_1,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) = c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a),
file('theBenchmark.p',cls_empty__is__image_1) ).
cnf(cls_insert__Diff_0,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))) = V_A ),
file('theBenchmark.p',cls_insert__Diff_0) ).
cnf(cls_image__constant__conv_1,axiom,
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool))
| c_Set_Oimage(c_COMBK(V_c,T_a,T_b),V_A,T_b,T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) ),
file('theBenchmark.p',cls_image__constant__conv_1) ).
cnf(cls_UN__insert_0,axiom,
c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(hAPP(hAPP(c_Set_Oinsert(T_b),V_a),V_A),V_B,T_b,tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(V_B,V_a)),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_B,T_b,tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_UN__insert_0) ).
cnf(cls_fold1__belowI_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ hBOOL(c_in(V_a,V_A,T_a))
| c_lessequals(c_Finite__Set_Ofold1(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_A,T_a),V_a,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_fold1__belowI_0) ).
cnf(cls_Inf__lower_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(c_Complete__Lattice_OInf__class_OInf(V_A,T_a),V_x,T_a)
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Inf__lower_0) ).
cnf(cls_atLeastatMost__empty__iff2_1,axiom,
( c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) = c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__empty__iff2_1) ).
cnf(cls_atLeastatMost__empty__iff2_0,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
cnf(cls_Int__insert__left_0,axiom,
( ~ hBOOL(c_in(V_a,V_C,T_a))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)),V_C) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C)) ),
file('theBenchmark.p',cls_Int__insert__left_0) ).
cnf(cls_Int__insert__right_0,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)) ),
file('theBenchmark.p',cls_Int__insert__right_0) ).
cnf(cls_Un__mono_0,axiom,
( ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_D,tc_fun(T_a,tc_bool))
| c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_C),V_D),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__mono_0) ).
cnf(cls_inf__sup__ord_I1_J_0,axiom,
( c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y),V_x,T_a)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__ord_I1_J_0) ).
cnf(cls_inf__sup__ord_I2_J_0,axiom,
( c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y),V_y,T_a)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__ord_I2_J_0) ).
cnf(cls_inf__greatest_0,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_x,V_z,T_a)
| c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z),T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__greatest_0) ).
cnf(cls_le__inf__iff_2,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_x,V_z,T_a)
| c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z),T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__inf__iff_2) ).
cnf(cls_le__infI_0,axiom,
( ~ c_lessequals(V_x,V_a,T_a)
| ~ c_lessequals(V_x,V_b,T_a)
| c_lessequals(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),V_b),T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_le__infI_0) ).
cnf(cls_inf__le2_0,axiom,
( c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y),V_y,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__le2_0) ).
cnf(cls_inf__le1_0,axiom,
( c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y),V_x,T_a)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__le1_0) ).
cnf(cls_Int__lower1_0,axiom,
c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),V_A,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Int__lower1_0) ).
cnf(cls_Int__lower2_0,axiom,
c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),V_B,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Int__lower2_0) ).
cnf(cls_Int__greatest_0,axiom,
( ~ c_lessequals(V_C,V_A,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_C,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_C,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Int__greatest_0) ).
cnf(cls_Int__subset__iff_2,axiom,
( ~ c_lessequals(V_C,V_A,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_C,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_C,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Int__subset__iff_2) ).
cnf(cls_o__assoc_0,axiom,
c_Fun_Ocomp(V_f,c_Fun_Ocomp(V_g,V_h,T_d,T_c,T_a),T_c,T_b,T_a) = c_Fun_Ocomp(c_Fun_Ocomp(V_f,V_g,T_c,T_b,T_d),V_h,T_d,T_b,T_a),
file('theBenchmark.p',cls_o__assoc_0) ).
cnf(cls_com_Osimps_I13_J_0,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('theBenchmark.p',cls_com_Osimps_I13_J_0) ).
cnf(cls_sup__inf__distrib2_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z)),V_x) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_y),V_x)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_z),V_x))
| ~ class_Lattices_Odistrib__lattice(T_a) ),
file('theBenchmark.p',cls_sup__inf__distrib2_0) ).
cnf(cls_sup__inf__distrib1_0,axiom,
( hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_y),V_z)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_z))
| ~ class_Lattices_Odistrib__lattice(T_a) ),
file('theBenchmark.p',cls_sup__inf__distrib1_0) ).
cnf(cls_Un__Int__distrib_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_C)),
file('theBenchmark.p',cls_Un__Int__distrib_0) ).
cnf(cls_Un__Int__distrib2_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C)),V_A) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_A)),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_C),V_A)),
file('theBenchmark.p',cls_Un__Int__distrib2_0) ).
cnf(cls_o__def_0,axiom,
hAPP(c_Fun_Ocomp(V_f,V_g,T_c,T_b,t_a),v_x) = hAPP(V_f,hAPP(V_g,v_x)),
file('theBenchmark.p',cls_o__def_0) ).
cnf(cls_insert__subset_2,axiom,
( ~ hBOOL(c_in(V_x,V_B,T_a))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_insert__subset_2) ).
cnf(cls_image__image_0,axiom,
c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
file('theBenchmark.p',cls_image__image_0) ).
cnf(cls_inf__sup__aci_I4_J_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)
| ~ class_Lattices_Olattice(T_a) ),
file('theBenchmark.p',cls_inf__sup__aci_I4_J_0) ).
cnf(cls_inf__left__idem_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_y)
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__left__idem_0) ).
cnf(cls_Int__left__absorb_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),
file('theBenchmark.p',cls_Int__left__absorb_0) ).
cnf(cls_fun__left__comm__idem_Ofun__left__idem_0,axiom,
( ~ c_Finite__Set_Ofun__left__comm__idem(V_f,T_a,T_b)
| hAPP(hAPP(V_f,V_x),hAPP(hAPP(V_f,V_x),V_z)) = hAPP(hAPP(V_f,V_x),V_z) ),
file('theBenchmark.p',cls_fun__left__comm__idem_Ofun__left__idem_0) ).
cnf(cls_finite__Diff__insert_0,axiom,
( ~ c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)),T_a)
| c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ),
file('theBenchmark.p',cls_finite__Diff__insert_0) ).
cnf(cls_finite__Diff__insert_1,axiom,
( ~ c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)),T_a) ),
file('theBenchmark.p',cls_finite__Diff__insert_1) ).
cnf(cls_image__compose_0,axiom,
c_Set_Oimage(c_Fun_Ocomp(V_f,V_g,T_c,T_a,T_b),V_r,T_b,T_a) = c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_r,T_b,T_c),T_c,T_a),
file('theBenchmark.p',cls_image__compose_0) ).
cnf(cls_com_Osimps_I47_J_0,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('theBenchmark.p',cls_com_Osimps_I47_J_0) ).
cnf(cls_UnCI_0,axiom,
( ~ hBOOL(c_in(V_c,V_B,T_a))
| hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a)) ),
file('theBenchmark.p',cls_UnCI_0) ).
cnf(cls_UnCI_1,axiom,
( ~ hBOOL(c_in(V_c,V_A,T_a))
| hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),T_a)) ),
file('theBenchmark.p',cls_UnCI_1) ).
cnf(cls_inf__idem_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_x),V_x) = V_x
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('theBenchmark.p',cls_inf__idem_0) ).
cnf(cls_Int__absorb_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_A) = V_A,
file('theBenchmark.p',cls_Int__absorb_0) ).
cnf(cls_le__sup__iff_1,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),V_z,T_a)
| c_lessequals(V_y,V_z,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__sup__iff_1) ).
cnf(cls_le__sup__iff_0,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_x),V_y),V_z,T_a)
| c_lessequals(V_x,V_z,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__sup__iff_0) ).
cnf(cls_le__supI2_0,axiom,
( ~ c_lessequals(V_x,V_b,T_a)
| c_lessequals(V_x,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),V_b),T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__supI2_0) ).
cnf(cls_le__supI1_0,axiom,
( ~ c_lessequals(V_x,V_a,T_a)
| c_lessequals(V_x,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),V_b),T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__supI1_0) ).
cnf(cls_le__supE_1,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),V_b),V_x,T_a)
| c_lessequals(V_b,V_x,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__supE_1) ).
cnf(cls_le__supE_0,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),V_b),V_x,T_a)
| c_lessequals(V_a,V_x,T_a)
| ~ class_Lattices_Oupper__semilattice(T_a) ),
file('theBenchmark.p',cls_le__supE_0) ).
cnf(cls_Un__subset__iff_0,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_C,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__subset__iff_0) ).
cnf(cls_Un__subset__iff_1,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),V_C,tc_fun(T_a,tc_bool))
| c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Un__subset__iff_1) ).
cnf(cls_Max__in_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| hBOOL(c_in(c_Finite__Set_Olinorder__class_OMax(V_A,T_a),V_A,T_a))
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Max__in_0) ).
cnf(cls_inf__fun__eq_0,axiom,
( hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(t_a,T_b)),V_f),V_g),v_x) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_b),hAPP(V_f,v_x)),hAPP(V_g,v_x))
| ~ class_Lattices_Olattice(T_b) ),
file('theBenchmark.p',cls_inf__fun__eq_0) ).
cnf(cls_xt1_I6_J_0,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_lessequals(V_z,V_y,T_a)
| c_lessequals(V_z,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_xt1_I6_J_0) ).
cnf(cls_order__trans_0,axiom,
( ~ c_lessequals(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_z,T_a)
| c_lessequals(V_x,V_z,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('theBenchmark.p',cls_order__trans_0) ).
cnf(cls_set__mp_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| hBOOL(c_in(V_x,V_B,T_a)) ),
file('theBenchmark.p',cls_set__mp_0) ).
cnf(cls_subsetD_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_c,V_A,T_a))
| hBOOL(c_in(V_c,V_B,T_a)) ),
file('theBenchmark.p',cls_subsetD_0) ).
cnf(cls_equalityE_0,axiom,
c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_equalityE_0) ).
cnf(cls_set__rev__mp_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| hBOOL(c_in(V_x,V_B,T_a)) ),
file('theBenchmark.p',cls_set__rev__mp_0) ).
cnf(cls_subset__iff_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ hBOOL(c_in(V_t,V_A,T_a))
| hBOOL(c_in(V_t,V_B,T_a)) ),
file('theBenchmark.p',cls_subset__iff_0) ).
cnf(cls_subset__refl_0,axiom,
c_lessequals(V_A,V_A,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_subset__refl_0) ).
cnf(cls_subset__trans_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__trans_0) ).
cnf(cls_subset__inj__on_0,axiom,
( ~ c_Fun_Oinj__on(V_f,V_B,T_a,T_b)
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Fun_Oinj__on(V_f,V_A,T_a,T_b) ),
file('theBenchmark.p',cls_subset__inj__on_0) ).
cnf(cls_predicate1D_0,axiom,
( ~ c_lessequals(V_P,V_Q,tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(V_P,V_x))
| hBOOL(hAPP(V_Q,V_x)) ),
file('theBenchmark.p',cls_predicate1D_0) ).
cnf(cls_order__eq__iff_0,axiom,
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_order__eq__iff_0) ).
cnf(cls_order__eq__refl_0,axiom,
( c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('theBenchmark.p',cls_order__eq__refl_0) ).
cnf(cls_finite__subset_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ c_Finite__Set_Ofinite(V_B,T_a)
| c_Finite__Set_Ofinite(V_A,T_a) ),
file('theBenchmark.p',cls_finite__subset_0) ).
cnf(cls_rev__predicate1D_0,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| ~ c_lessequals(V_P,V_Q,tc_fun(T_a,tc_bool))
| hBOOL(hAPP(V_Q,V_x)) ),
file('theBenchmark.p',cls_rev__predicate1D_0) ).
cnf(cls_rev__finite__subset_0,axiom,
( ~ c_Finite__Set_Ofinite(V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Finite__Set_Ofinite(V_A,T_a) ),
file('theBenchmark.p',cls_rev__finite__subset_0) ).
cnf(cls_Int__mono_0,axiom,
( ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_D,tc_fun(T_a,tc_bool))
| c_lessequals(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_C),V_D),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_Int__mono_0) ).
cnf(cls_Diff__Un_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C),tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))),c_HOL_Ominus__class_Ominus(V_A,V_C,tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_Diff__Un_0) ).
cnf(cls_atLeastatMost__empty__iff_1,axiom,
( c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__empty__iff_1) ).
cnf(cls_atLeastatMost__empty__iff_0,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
cnf(cls_Int__Diff_0,axiom,
c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),V_C,tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),c_HOL_Ominus__class_Ominus(V_B,V_C,tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_Int__Diff_0) ).
cnf(cls_inj__on__image__set__diff_0,axiom,
( ~ c_Fun_Oinj__on(V_f,V_C,T_a,T_b)
| ~ c_lessequals(V_A,V_C,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
| c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a,T_b) = c_HOL_Ominus__class_Ominus(c_Set_Oimage(V_f,V_A,T_a,T_b),c_Set_Oimage(V_f,V_B,T_a,T_b),tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_inj__on__image__set__diff_0) ).
cnf(cls_Min__in_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| hBOOL(c_in(c_Finite__Set_Olinorder__class_OMin(V_A,T_a),V_A,T_a))
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Min__in_0) ).
cnf(cls_Int__Collect_2,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(hAPP(V_P,V_x))
| hBOOL(c_in(V_x,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),c_Collect(V_P,T_a)),T_a)) ),
file('theBenchmark.p',cls_Int__Collect_2) ).
cnf(cls_o__eq__dest_0,axiom,
( hAPP(V_a,hAPP(V_b,V_v)) = hAPP(V_c,hAPP(V_d,V_v))
| c_Fun_Ocomp(V_a,V_b,T_c,T_b,T_a) != c_Fun_Ocomp(V_c,V_d,T_d,T_b,T_a) ),
file('theBenchmark.p',cls_o__eq__dest_0) ).
cnf(cls_comp__cong_0,axiom,
( hAPP(c_Fun_Ocomp(V_f,V_g,T_b,T_a,T_c),V_x) = hAPP(c_Fun_Ocomp(V_f_H,V_g_H,T_d,T_a,T_e),V_x_H)
| hAPP(V_f,hAPP(V_g,V_x)) != hAPP(V_f_H,hAPP(V_g_H,V_x_H)) ),
file('theBenchmark.p',cls_comp__cong_0) ).
cnf(cls_Diff__Int_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_B),V_C),tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))),c_HOL_Ominus__class_Ominus(V_A,V_C,tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_Diff__Int_0) ).
cnf(cls_UN__Un_0,axiom,
c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_b,tc_bool)),V_A),V_B),V_M,T_b,tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_A,V_M,T_b,tc_fun(T_a,tc_bool))),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(V_B,V_M,T_b,tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_UN__Un_0) ).
cnf(cls_the__sym__eq__trivial_0,axiom,
c_The(c_fequal(V_x,T_a),T_a) = V_x,
file('theBenchmark.p',cls_the__sym__eq__trivial_0) ).
cnf(cls_linorder_Onot__less__iff__gr__or__eq_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| V_x = V_y ),
file('theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_0) ).
cnf(cls_linorder_OneqE_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| V_x = V_y
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| hBOOL(hAPP(hAPP(V_less,V_y),V_x)) ),
file('theBenchmark.p',cls_linorder_OneqE_0) ).
cnf(cls_linorder_Oless__linear_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| V_x = V_y
| hBOOL(hAPP(hAPP(V_less,V_y),V_x)) ),
file('theBenchmark.p',cls_linorder_Oless__linear_0) ).
cnf(cls_linorder_Oantisym__conv3_0,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| hBOOL(hAPP(hAPP(V_less,V_x),V_y))
| V_x = V_y ),
file('theBenchmark.p',cls_linorder_Oantisym__conv3_0) ).
cnf(cls_Min__le_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(c_Finite__Set_Olinorder__class_OMin(V_A,T_a),V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Min__le_0) ).
cnf(cls_IntI_0,axiom,
( ~ hBOOL(c_in(V_c,V_A,T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a))
| hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),T_a)) ),
file('theBenchmark.p',cls_IntI_0) ).
cnf(cls_Int__iff_2,axiom,
( ~ hBOOL(c_in(V_c,V_A,T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a))
| hBOOL(c_in(V_c,hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),T_a)) ),
file('theBenchmark.p',cls_Int__iff_2) ).
cnf(cls_inf1I_0,axiom,
( ~ hBOOL(hAPP(V_A,V_x))
| ~ hBOOL(hAPP(V_B,V_x))
| hBOOL(hAPP(hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B),V_x)) ),
file('theBenchmark.p',cls_inf1I_0) ).
cnf(cls_fun__left__comm__idem_Ofun__comp__idem_0,axiom,
( ~ c_Finite__Set_Ofun__left__comm__idem(V_f,T_a,T_b)
| c_Fun_Ocomp(hAPP(V_f,V_x),hAPP(V_f,V_x),T_b,T_b,T_b) = hAPP(V_f,V_x) ),
file('theBenchmark.p',cls_fun__left__comm__idem_Ofun__comp__idem_0) ).
cnf(cls_double__diff_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_B,V_C,tc_fun(T_a,tc_bool))
| c_HOL_Ominus__class_Ominus(V_B,c_HOL_Ominus__class_Ominus(V_C,V_A,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = V_A ),
file('theBenchmark.p',cls_double__diff_0) ).
cnf(cls_le__eqI_0,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| c_lessequals(V_y_H,V_x_H,T_a)
| c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add(T_a) ),
file('theBenchmark.p',cls_le__eqI_0) ).
cnf(cls_le__eqI_1,axiom,
( ~ c_lessequals(V_y_H,V_x_H,T_a)
| c_lessequals(V_y,V_x,T_a)
| c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a)
| ~ class_OrderedGroup_Opordered__ab__group__add(T_a) ),
file('theBenchmark.p',cls_le__eqI_1) ).
cnf(cls_image__mono_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oimage(V_f,V_A,T_a,T_b),c_Set_Oimage(V_f,V_B,T_a,T_b),tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_image__mono_0) ).
cnf(cls_subset__image__iff_2,axiom,
( c_lessequals(c_Set_Oimage(V_f,V_x,T_b,T_a),c_Set_Oimage(V_f,V_A,T_b,T_a),tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_x,V_A,tc_fun(T_b,tc_bool)) ),
file('theBenchmark.p',cls_subset__image__iff_2) ).
cnf(cls_ivl__disj__int_I4_J_0,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),c_SetInterval_Oord__class_OlessThan(V_l,T_a)),c_SetInterval_Oord__class_OatLeastAtMost(V_l,V_u,T_a)) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_ivl__disj__int_I4_J_0) ).
cnf(cls_finite__imageD_0,axiom,
( ~ c_Finite__Set_Ofinite(c_Set_Oimage(V_f,V_A,T_b,T_a),T_a)
| ~ c_Fun_Oinj__on(V_f,V_A,T_b,T_a)
| c_Finite__Set_Ofinite(V_A,T_b) ),
file('theBenchmark.p',cls_finite__imageD_0) ).
cnf(cls_Max__ge_0,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(V_x,c_Finite__Set_Olinorder__class_OMax(V_A,T_a),T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Max__ge_0) ).
cnf(cls_image__Un_0,axiom,
c_Set_Oimage(V_f,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_b,tc_bool)),V_A),V_B),T_b,T_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Set_Oimage(V_f,V_A,T_b,T_a)),c_Set_Oimage(V_f,V_B,T_b,T_a)),
file('theBenchmark.p',cls_image__Un_0) ).
cnf(cls_Sup__upper_0,axiom,
( ~ hBOOL(c_in(V_x,V_A,T_a))
| c_lessequals(V_x,c_Complete__Lattice_OSup__class_OSup(V_A,T_a),T_a)
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Sup__upper_0) ).
cnf(cls_com_Osimps_I12_J_0,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('theBenchmark.p',cls_com_Osimps_I12_J_0) ).
cnf(cls_linorder__linear_0,axiom,
( c_lessequals(V_x,V_y,T_a)
| c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_linorder__linear_0) ).
cnf(cls_Sup__binary_0,axiom,
( c_Complete__Lattice_OSup__class_OSup(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),T_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(T_a),V_a),V_b)
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Sup__binary_0) ).
cnf(cls_linorder_OMax__singleton_0,axiom,
( c_Finite__Set_Ofold1(V_f,hAPP(hAPP(c_Set_Oinsert(T_b),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool))),T_b) = V_a
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
file('theBenchmark.p',cls_linorder_OMax__singleton_0) ).
cnf(cls_single__Diff__lessThan_0,axiom,
( c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Set_Oinsert(T_a),V_k),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),c_SetInterval_Oord__class_OlessThan(V_k,T_a),tc_fun(T_a,tc_bool)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_k),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_single__Diff__lessThan_0) ).
cnf(cls_subset__insert__iff_4,axiom,
( ~ c_lessequals(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool))
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insert__iff_4) ).
cnf(cls_Diff__insert__absorb_0,axiom,
( hBOOL(c_in(V_x,V_A,T_a))
| c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)) = V_A ),
file('theBenchmark.p',cls_Diff__insert__absorb_0) ).
cnf(cls_Inf__binary_0,axiom,
( c_Complete__Lattice_OInf__class_OInf(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),T_a) = hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(T_a),V_a),V_b)
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Inf__binary_0) ).
cnf(cls_insert__mono_0,axiom,
( ~ c_lessequals(V_C,V_D,tc_fun(T_a,tc_bool))
| c_lessequals(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_C),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_D),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_insert__mono_0) ).
cnf(cls_insert__iff_2,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| hBOOL(c_in(V_a,hAPP(hAPP(c_Set_Oinsert(T_a),V_b),V_A),T_a)) ),
file('theBenchmark.p',cls_insert__iff_2) ).
cnf(cls_insertCI_0,axiom,
( ~ hBOOL(c_in(V_a,V_B,T_a))
| hBOOL(c_in(V_a,hAPP(hAPP(c_Set_Oinsert(T_a),V_b),V_B),T_a)) ),
file('theBenchmark.p',cls_insertCI_0) ).
cnf(cls_image__insert_0,axiom,
c_Set_Oimage(V_f,hAPP(hAPP(c_Set_Oinsert(T_b),V_a),V_B),T_b,T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),hAPP(V_f,V_a)),c_Set_Oimage(V_f,V_B,T_b,T_a)),
file('theBenchmark.p',cls_image__insert_0) ).
cnf(cls_complete__lattice_OInf__insert_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Inf,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A)) = hAPP(hAPP(V_inf,V_a),hAPP(V_Inf,V_A)) ),
file('theBenchmark.p',cls_complete__lattice_OInf__insert_0) ).
cnf(cls_complete__lattice_OSup__insert_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Sup,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A)) = hAPP(hAPP(V_sup,V_a),hAPP(V_Sup,V_A)) ),
file('theBenchmark.p',cls_complete__lattice_OSup__insert_0) ).
cnf(cls_insertE_0,axiom,
( ~ hBOOL(c_in(V_a,hAPP(hAPP(c_Set_Oinsert(T_a),V_b),V_A),T_a))
| V_a = V_b
| hBOOL(c_in(V_a,V_A,T_a)) ),
file('theBenchmark.p',cls_insertE_0) ).
cnf(cls_finite__insert_1,axiom,
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ofinite(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a) ),
file('theBenchmark.p',cls_finite__insert_1) ).
cnf(cls_finite__insert_0,axiom,
( ~ c_Finite__Set_Ofinite(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a)
| c_Finite__Set_Ofinite(V_A,T_a) ),
file('theBenchmark.p',cls_finite__insert_0) ).
cnf(cls_subset__insertI_0,axiom,
c_lessequals(V_B,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_subset__insertI_0) ).
cnf(cls_insert__inter__insert_0,axiom,
hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B)),
file('theBenchmark.p',cls_insert__inter__insert_0) ).
cnf(cls_Un__insert__right_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B)),
file('theBenchmark.p',cls_Un__insert__right_0) ).
cnf(cls_Un__insert__left_0,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B)),V_C) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C)),
file('theBenchmark.p',cls_Un__insert__left_0) ).
cnf(cls_subset__insertI2_0,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_b),V_B),tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_subset__insertI2_0) ).
cnf(cls_insert__subset_1,axiom,
( ~ c_lessequals(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),V_B,tc_fun(T_a,tc_bool))
| c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_insert__subset_1) ).
cnf(cls_inj__on__insert_0,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| c_Fun_Oinj__on(V_f,V_A,T_a,T_b) ),
file('theBenchmark.p',cls_inj__on__insert_0) ).
cnf(cls_insert__iff_1,axiom,
hBOOL(c_in(V_x,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),T_a)),
file('theBenchmark.p',cls_insert__iff_1) ).
cnf(cls_insertI1_0,axiom,
hBOOL(c_in(V_a,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),T_a)),
file('theBenchmark.p',cls_insertI1_0) ).
cnf(cls_insertCI_1,axiom,
hBOOL(c_in(V_x,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B),T_a)),
file('theBenchmark.p',cls_insertCI_1) ).
cnf(cls_fun__left__comm__idem__insert_0,axiom,
c_Finite__Set_Ofun__left__comm__idem(c_Set_Oinsert(T_a),T_a,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_fun__left__comm__idem__insert_0) ).
cnf(cls_insert__ident_0,axiom,
( V_A = V_B
| hBOOL(c_in(V_x,V_A,T_a))
| hBOOL(c_in(V_x,V_B,T_a))
| hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A) != hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_B) ),
file('theBenchmark.p',cls_insert__ident_0) ).
cnf(cls_insert__absorb_0,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) = V_A ),
file('theBenchmark.p',cls_insert__absorb_0) ).
cnf(cls_triple_Osplit__asm_0,axiom,
( hBOOL(hAPP(V_P,hAPP(hAPP(hAPP(V_f1,V_xa),V_xb),V_xc)))
| ~ hBOOL(hAPP(V_P,c_Hoare__Mirabelle_Otriple_Otriple__case(V_f1,c_Hoare__Mirabelle_Otriple_Otriple(V_xa,V_xb,V_xc,t_b),t_b,t_a))) ),
file('theBenchmark.p',cls_triple_Osplit__asm_0) ).
cnf(cls_triple_Osplit_0,axiom,
( hBOOL(hAPP(V_P,hAPP(hAPP(hAPP(V_f1,V_fun1),V_com),V_fun2)))
| ~ hBOOL(hAPP(V_P,c_Hoare__Mirabelle_Otriple_Otriple__case(V_f1,c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,t_b),t_b,t_a))) ),
file('theBenchmark.p',cls_triple_Osplit_0) ).
cnf(cls_triple_Orecs_0,axiom,
c_Hoare__Mirabelle_Otriple_Otriple__rec(V_f1,c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_b),T_b,T_a) = hAPP(hAPP(hAPP(V_f1,V_fun1),V_com),V_fun2),
file('theBenchmark.p',cls_triple_Orecs_0) ).
cnf(cls_triple_Ocases_0,axiom,
c_Hoare__Mirabelle_Otriple_Otriple__case(V_f1,c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_b),T_b,T_a) = hAPP(hAPP(hAPP(V_f1,V_fun1),V_com),V_fun2),
file('theBenchmark.p',cls_triple_Ocases_0) ).
cnf(cls_COMBI__def__raw_0,axiom,
hAPP(c_COMBI(t_a),v_P) = v_P,
file('theBenchmark.p',cls_COMBI__def__raw_0) ).
cnf(cls_weaken_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts_H,T_a)
| ~ c_lessequals(V_ts,V_ts_H,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('theBenchmark.p',cls_weaken_0) ).
cnf(cls_asm_0,axiom,
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('theBenchmark.p',cls_asm_0) ).
cnf(cls_COMBB__def__raw_0,axiom,
hAPP(c_COMBB(v_P,v_Q,t_a,t_b,t_c),v_R) = hAPP(v_P,hAPP(v_Q,v_R)),
file('theBenchmark.p',cls_COMBB__def__raw_0) ).
cnf(cls_COMBS__def__raw_0,axiom,
c_COMBS(v_P,v_Q,v_R,t_a,t_b,t_c) = hAPP(hAPP(v_P,v_R),hAPP(v_Q,v_R)),
file('theBenchmark.p',cls_COMBS__def__raw_0) ).
cnf(cls_COMBC__def__raw_0,axiom,
c_COMBC(v_P,v_Q,v_R,t_a,t_b,t_c) = hAPP(hAPP(v_P,v_R),v_Q),
file('theBenchmark.p',cls_COMBC__def__raw_0) ).
cnf(cls_Loop_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_Hoare__Mirabelle_Opeek__and(V_P,V_b,T_a),V_c,V_P,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Com_Ocom_OWhile(V_b,V_c),c_Hoare__Mirabelle_Opeek__and(V_P,c_Fun_Ocomp(c_Not,V_b,tc_bool,tc_bool,tc_Com_Ostate),T_a),T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a) ),
file('theBenchmark.p',cls_Loop_0) ).
cnf(cls_hoare__derivs_OIf_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_Hoare__Mirabelle_Opeek__and(V_P,V_b,T_a),V_c,V_Q,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(c_Hoare__Mirabelle_Opeek__and(V_P,c_Fun_Ocomp(c_Not,V_b,tc_bool,tc_bool,tc_Com_Ostate),T_a),V_d,V_Q,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Com_Ocom_OCond(V_b,V_c,V_d),V_Q,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a) ),
file('theBenchmark.p',cls_hoare__derivs_OIf_0) ).
cnf(cls_bot__fun__eq_0,axiom,
( hAPP(c_Orderings_Obot__class_Obot(tc_fun(t_a,T_b)),v_x) = c_Orderings_Obot__class_Obot(T_b)
| ~ class_Orderings_Obot(T_b) ),
file('theBenchmark.p',cls_bot__fun__eq_0) ).
cnf(cls_Sup__empty_0,axiom,
( c_Complete__Lattice_OSup__class_OSup(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) = c_Orderings_Obot__class_Obot(T_a)
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Sup__empty_0) ).
cnf(cls_singleton__conv2_0,axiom,
c_Collect(c_fequal(V_a,T_a),T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_singleton__conv2_0) ).
cnf(cls_subset__singletonD_0,axiom,
( ~ c_lessequals(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))
| V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| V_A = hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) ),
file('theBenchmark.p',cls_subset__singletonD_0) ).
cnf(cls_singleton__iff_1,axiom,
hBOOL(c_in(V_x,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a)),
file('theBenchmark.p',cls_singleton__iff_1) ).
cnf(cls_complete__lattice_OInf__singleton_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Inf,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) = V_a ),
file('theBenchmark.p',cls_complete__lattice_OInf__singleton_0) ).
cnf(cls_complete__lattice_OSup__singleton_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Sup,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) = V_a ),
file('theBenchmark.p',cls_complete__lattice_OSup__singleton_0) ).
cnf(cls_Sup__singleton_0,axiom,
( c_Complete__Lattice_OSup__class_OSup(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_a
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Sup__singleton_0) ).
cnf(cls_Nitpick_OEx1__def_2,axiom,
hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),c_Nitpick_Osko__Nitpick__XEx1__def__1__3(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a))),
file('theBenchmark.p',cls_Nitpick_OEx1__def_2) ).
cnf(cls_UN__extend__simps_I1_J_0,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),V_B,T_b,tc_fun(T_a,tc_bool))) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),
file('theBenchmark.p',cls_UN__extend__simps_I1_J_0) ).
cnf(cls_fold1Set__sing_1,axiom,
hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a),V_x)),
file('theBenchmark.p',cls_fold1Set__sing_1) ).
cnf(cls_Min__singleton_0,axiom,
( c_Finite__Set_Olinorder__class_OMin(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_a
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Min__singleton_0) ).
cnf(cls_Nitpick_OThe__psimp_0,axiom,
c_The(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_x,
file('theBenchmark.p',cls_Nitpick_OThe__psimp_0) ).
cnf(cls_complete__lattice_OInf__binary_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Inf,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))) = hAPP(hAPP(V_inf,V_a),V_b) ),
file('theBenchmark.p',cls_complete__lattice_OInf__binary_0) ).
cnf(cls_complete__lattice_OSup__binary_0,axiom,
( ~ c_Complete__Lattice_Ocomplete__lattice(V_Inf,V_Sup,V_less__eq,V_less,V_inf,V_sup,V_bot,V_top,T_a)
| hAPP(V_Sup,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))) = hAPP(hAPP(V_sup,V_a),V_b) ),
file('theBenchmark.p',cls_complete__lattice_OSup__binary_0) ).
cnf(cls_Diff__insert2_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__insert2_0) ).
cnf(cls_Diff__insert_0,axiom,
c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_B),tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_Diff__insert_0) ).
cnf(cls_fold1Set__sing_0,axiom,
( ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a),V_b))
| V_a = V_b ),
file('theBenchmark.p',cls_fold1Set__sing_0) ).
cnf(cls_contents__eq_0,axiom,
c_Set_Ocontents(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_x,
file('theBenchmark.p',cls_contents__eq_0) ).
cnf(cls_Nitpick_OEx1__def_3,axiom,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),V_y))
| V_y = c_Nitpick_Osko__Nitpick__XEx1__def__1__3(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) ),
file('theBenchmark.p',cls_Nitpick_OEx1__def_3) ).
cnf(cls_singletonE_0,axiom,
( ~ hBOOL(c_in(V_b,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a))
| V_b = V_a ),
file('theBenchmark.p',cls_singletonE_0) ).
cnf(cls_fold1__singleton_0,axiom,
c_Finite__Set_Ofold1(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_a,
file('theBenchmark.p',cls_fold1__singleton_0) ).
cnf(cls_Max__singleton_0,axiom,
( c_Finite__Set_Olinorder__class_OMax(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_a
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_Max__singleton_0) ).
cnf(cls_insert__Diff__single_0,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
file('theBenchmark.p',cls_insert__Diff__single_0) ).
cnf(cls_atLeastAtMost__singleton_0,axiom,
( c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_a,T_a) = hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_atLeastAtMost__singleton_0) ).
cnf(cls_comm__monoid__add_Ononempty__iff_2,axiom,
( hBOOL(c_in(V_x,V_xa,T_a))
| hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_xa) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('theBenchmark.p',cls_comm__monoid__add_Ononempty__iff_2) ).
cnf(cls_insert__is__Un_0,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),V_A),
file('theBenchmark.p',cls_insert__is__Un_0) ).
cnf(cls_Inf__singleton_0,axiom,
( c_Complete__Lattice_OInf__class_OInf(hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),T_a) = V_a
| ~ class_Complete__Lattice_Ocomplete__lattice(T_a) ),
file('theBenchmark.p',cls_Inf__singleton_0) ).
cnf(cls_conseq_1,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_x,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(V_G,V_P,V_Q,V_c)))
| hBOOL(hAPP(hAPP(V_xa,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_conseq_1) ).
cnf(cls_conseq12_1,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P_H,V_c,V_Q_H,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_P_H,V_Z_H),v_sko__Hoare__Mirabelle__Xconseq12__2(V_P,V_P_H,V_Q,V_Q_H)))
| hBOOL(hAPP(hAPP(V_Q_H,V_Z_H),v_sko__Hoare__Mirabelle__Xconseq12__3(V_P,V_P_H,V_Q,V_Q_H)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_conseq12_1) ).
cnf(cls_hoare__derivs_Ointros_I6_J_1,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_x,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(V_G,V_P,V_Q,V_c)))
| hBOOL(hAPP(hAPP(V_xa,V_Z_H),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_hoare__derivs_Ointros_I6_J_1) ).
cnf(cls_hoare__derivs_Ointros_I6_J_0,axiom,
( hBOOL(hAPP(hAPP(V_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(V_G,V_P,V_Q,V_c)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_hoare__derivs_Ointros_I6_J_0) ).
cnf(cls_hoare__derivs_Ointros_I6_J_2,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_hoare__derivs_Ointros_I6_J_2) ).
cnf(cls_conseq_0,axiom,
( hBOOL(hAPP(hAPP(V_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(V_G,V_P,V_Q,V_c)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_conseq_0) ).
cnf(cls_conseq12_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P_H,V_c,V_Q_H,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| hBOOL(hAPP(hAPP(V_P,v_sko__Hoare__Mirabelle__Xconseq12__1(V_P,V_P_H,V_Q,V_Q_H)),v_sko__Hoare__Mirabelle__Xconseq12__2(V_P,V_P_H,V_Q,V_Q_H)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_conseq12_0) ).
cnf(cls_conseq_2,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_x,V_c,V_xa,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(V_G,V_P,V_Q,V_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(V_G,V_P,V_Q,V_c,V_x,V_xa)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_conseq_2) ).
cnf(cls_conseq12_2,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P_H,V_c,V_Q_H,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(V_Q,v_sko__Hoare__Mirabelle__Xconseq12__1(V_P,V_P_H,V_Q,V_Q_H)),v_sko__Hoare__Mirabelle__Xconseq12__3(V_P,V_P_H,V_Q,V_Q_H)))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('theBenchmark.p',cls_conseq12_2) ).
cnf(cls_COMBK__def__raw_0,axiom,
hAPP(c_COMBK(v_P,t_a,t_b),v_Q) = v_P,
file('theBenchmark.p',cls_COMBK__def__raw_0) ).
cnf(cls_hoare__derivs_OSkip_0,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Com_Ocom_OSKIP,V_P,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a),
file('theBenchmark.p',cls_hoare__derivs_OSkip_0) ).
cnf(cls_Comp_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,V_c,V_Q,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_Q,V_d,V_R,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),c_Hoare__Mirabelle_Otriple_Otriple(V_P,c_Com_Ocom_OSemi(V_c,V_d),V_R,T_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a) ),
file('theBenchmark.p',cls_Comp_0) ).
cnf(cls_hoare__derivs_Oinsert_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))),T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(T_a)),V_t),V_ts),T_a) ),
file('theBenchmark.p',cls_hoare__derivs_Oinsert_0) ).
cnf(cls_insert__code_1,axiom,
hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),V_x)),
file('theBenchmark.p',cls_insert__code_1) ).
cnf(cls_cut_0,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G_H,V_ts,T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_G_H,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('theBenchmark.p',cls_cut_0) ).
cnf(cls_empty__not__insert_0,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
file('theBenchmark.p',cls_empty__not__insert_0) ).
cnf(cls_triple_Oinject_2,axiom,
( V_fun2 = V_fun2_H
| c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_a) != c_Hoare__Mirabelle_Otriple_Otriple(V_fun1_H,V_com_H,V_fun2_H,T_a) ),
file('theBenchmark.p',cls_triple_Oinject_2) ).
cnf(cls_triple_Oinject_1,axiom,
( V_com = V_com_H
| c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_a) != c_Hoare__Mirabelle_Otriple_Otriple(V_fun1_H,V_com_H,V_fun2_H,T_a) ),
file('theBenchmark.p',cls_triple_Oinject_1) ).
cnf(cls_triple_Oinject_0,axiom,
( V_fun1 = V_fun1_H
| c_Hoare__Mirabelle_Otriple_Otriple(V_fun1,V_com,V_fun2,T_a) != c_Hoare__Mirabelle_Otriple_Otriple(V_fun1_H,V_com_H,V_fun2_H,T_a) ),
file('theBenchmark.p',cls_triple_Oinject_0) ).
cnf(cls_doubleton__eq__iff_3,axiom,
( V_b = V_d
| V_b = V_c
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) != hAPP(hAPP(c_Set_Oinsert(T_a),V_c),hAPP(hAPP(c_Set_Oinsert(T_a),V_d),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) ),
file('theBenchmark.p',cls_doubleton__eq__iff_3) ).
cnf(cls_doubleton__eq__iff_2,axiom,
( V_b = V_d
| V_a = V_d
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) != hAPP(hAPP(c_Set_Oinsert(T_a),V_c),hAPP(hAPP(c_Set_Oinsert(T_a),V_d),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) ),
file('theBenchmark.p',cls_doubleton__eq__iff_2) ).
cnf(cls_doubleton__eq__iff_1,axiom,
( V_a = V_c
| V_b = V_c
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) != hAPP(hAPP(c_Set_Oinsert(T_a),V_c),hAPP(hAPP(c_Set_Oinsert(T_a),V_d),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) ),
file('theBenchmark.p',cls_doubleton__eq__iff_1) ).
cnf(cls_doubleton__eq__iff_0,axiom,
( V_a = V_c
| V_a = V_d
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) != hAPP(hAPP(c_Set_Oinsert(T_a),V_c),hAPP(hAPP(c_Set_Oinsert(T_a),V_d),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) ),
file('theBenchmark.p',cls_doubleton__eq__iff_0) ).
cnf(cls_bot1E_0,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('theBenchmark.p',cls_bot1E_0) ).
cnf(cls_empty_0,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
file('theBenchmark.p',cls_empty_0) ).
cnf(cls_insert__code_0,axiom,
( ~ hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_a),V_y),V_A),V_x))
| V_y = V_x
| hBOOL(hAPP(V_A,V_x)) ),
file('theBenchmark.p',cls_insert__code_0) ).
cnf(cls_insert__absorb2_0,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_x),hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A),
file('theBenchmark.p',cls_insert__absorb2_0) ).
cnf(cls_insert__not__empty_0,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('theBenchmark.p',cls_insert__not__empty_0) ).
cnf(cls_insert__commute_0,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_x),hAPP(hAPP(c_Set_Oinsert(T_a),V_y),V_A)) = hAPP(hAPP(c_Set_Oinsert(T_a),V_y),hAPP(hAPP(c_Set_Oinsert(T_a),V_x),V_A)),
file('theBenchmark.p',cls_insert__commute_0) ).
cnf(cls_doubleton__eq__iff_4,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_xa),hAPP(hAPP(c_Set_Oinsert(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))) = hAPP(hAPP(c_Set_Oinsert(T_a),V_x),hAPP(hAPP(c_Set_Oinsert(T_a),V_xa),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('theBenchmark.p',cls_doubleton__eq__iff_4) ).
cnf(cls_singleton__inject_0,axiom,
( V_a = V_b
| hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) != hAPP(hAPP(c_Set_Oinsert(T_a),V_b),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))) ),
file('theBenchmark.p',cls_singleton__inject_0) ).
cnf(cls_insert__code_2,axiom,
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(hAPP(hAPP(c_Set_Oinsert(T_a),V_y),V_A),V_x)) ),
file('theBenchmark.p',cls_insert__code_2) ).
cnf(cls_conjecture_0,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P_H,v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(cls_conjecture_1,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_2,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| hBOOL(hAPP(hAPP(v_P_H,V_Z),V_s)) ),
file('theBenchmark.p',cls_conjecture_2) ).
cnf(clsarity_fun__Complete__Lattice_Ocomplete__lattice,axiom,
( ~ class_Complete__Lattice_Ocomplete__lattice(T_1)
| class_Complete__Lattice_Ocomplete__lattice(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Complete__Lattice_Ocomplete__lattice) ).
cnf(clsarity_fun__Lattices_Oupper__semilattice,axiom,
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Oupper__semilattice(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Lattices_Oupper__semilattice) ).
cnf(clsarity_fun__Lattices_Olower__semilattice,axiom,
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Lattices_Olower__semilattice) ).
cnf(clsarity_fun__Lattices_Odistrib__lattice,axiom,
( ~ class_Lattices_Odistrib__lattice(T_1)
| class_Lattices_Odistrib__lattice(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Lattices_Odistrib__lattice) ).
cnf(clsarity_fun__Lattices_Obounded__lattice,axiom,
( ~ class_Lattices_Obounded__lattice(T_1)
| class_Lattices_Obounded__lattice(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Lattices_Obounded__lattice) ).
cnf(clsarity_fun__Finite__Set_Ofinite_Ofinite,axiom,
( ~ class_Finite__Set_Ofinite_Ofinite(T_2)
| ~ class_Finite__Set_Ofinite_Ofinite(T_1)
| class_Finite__Set_Ofinite_Ofinite(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Finite__Set_Ofinite_Ofinite) ).
cnf(clsarity_fun__Orderings_Opreorder,axiom,
( ~ class_Orderings_Opreorder(T_1)
| class_Orderings_Opreorder(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Orderings_Opreorder) ).
cnf(clsarity_fun__Lattices_Olattice,axiom,
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Olattice(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Lattices_Olattice) ).
cnf(clsarity_fun__Orderings_Oorder,axiom,
( ~ class_Orderings_Oorder(T_1)
| class_Orderings_Oorder(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Orderings_Oorder) ).
cnf(clsarity_fun__Orderings_Obot,axiom,
( ~ class_Orderings_Obot(T_1)
| class_Orderings_Obot(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__Orderings_Obot) ).
cnf(clsarity_fun__HOL_Ominus,axiom,
( ~ class_HOL_Ominus(T_1)
| class_HOL_Ominus(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__HOL_Ominus) ).
cnf(clsarity_fun__HOL_Oord,axiom,
( ~ class_HOL_Oord(T_1)
| class_HOL_Oord(tc_fun(T_2,T_1)) ),
file('theBenchmark.p',clsarity_fun__HOL_Oord) ).
cnf(clsarity_bool__Complete__Lattice_Ocomplete__lattice,axiom,
class_Complete__Lattice_Ocomplete__lattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Complete__Lattice_Ocomplete__lattice) ).
cnf(clsarity_bool__Lattices_Oupper__semilattice,axiom,
class_Lattices_Oupper__semilattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Lattices_Oupper__semilattice) ).
cnf(clsarity_bool__Lattices_Olower__semilattice,axiom,
class_Lattices_Olower__semilattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Lattices_Olower__semilattice) ).
cnf(clsarity_bool__Lattices_Odistrib__lattice,axiom,
class_Lattices_Odistrib__lattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Lattices_Odistrib__lattice) ).
cnf(clsarity_bool__Lattices_Obounded__lattice,axiom,
class_Lattices_Obounded__lattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Lattices_Obounded__lattice) ).
cnf(clsarity_bool__Finite__Set_Ofinite_Ofinite,axiom,
class_Finite__Set_Ofinite_Ofinite(tc_bool),
file('theBenchmark.p',clsarity_bool__Finite__Set_Ofinite_Ofinite) ).
cnf(clsarity_bool__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_bool),
file('theBenchmark.p',clsarity_bool__Orderings_Opreorder) ).
cnf(clsarity_bool__Lattices_Olattice,axiom,
class_Lattices_Olattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Lattices_Olattice) ).
cnf(clsarity_bool__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_bool),
file('theBenchmark.p',clsarity_bool__Orderings_Oorder) ).
cnf(clsarity_bool__Orderings_Obot,axiom,
class_Orderings_Obot(tc_bool),
file('theBenchmark.p',clsarity_bool__Orderings_Obot) ).
cnf(clsarity_bool__HOL_Ominus,axiom,
class_HOL_Ominus(tc_bool),
file('theBenchmark.p',clsarity_bool__HOL_Ominus) ).
cnf(clsarity_bool__HOL_Oord,axiom,
class_HOL_Oord(tc_bool),
file('theBenchmark.p',clsarity_bool__HOL_Oord) ).
cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom,
hBOOL(hAPP(c_fequal(V_x,T_a),V_x)),
file('theBenchmark.p',cls_ATP__Linkup_Oequal__imp__fequal_0) ).
cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom,
( ~ hBOOL(hAPP(c_fequal(V_X,T_a),V_Y))
| V_X = V_Y ),
file('theBenchmark.p',cls_ATP__Linkup_Ofequal__imp__equal_0) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( tc_fun(Eq_x_0,Eq_x_1) = tc_fun(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( c_Lattices_Olower__semilattice__class_Oinf(Eq_x_0) = c_Lattices_Olower__semilattice__class_Oinf(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( hAPP(Eq_x_0,Eq_x_1) = hAPP(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( c_Orderings_Obot__class_Obot(Eq_x_0) = c_Orderings_Obot__class_Obot(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( c_HOL_Ominus__class_Ominus(Eq_x_0,Eq_x_1,Eq_x_2) = c_HOL_Ominus__class_Ominus(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( c_Lattices_Oupper__semilattice__class_Osup(Eq_x_0) = c_Lattices_Oupper__semilattice__class_Osup(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( c_Set_Oimage(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = c_Set_Oimage(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( c_Fun_Ocomp(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = c_Fun_Ocomp(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( c_Collect(Eq_x_0,Eq_x_1) = c_Collect(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( c_in(Eq_x_0,Eq_x_1,Eq_x_2) = c_in(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( c_Set_Oinsert(Eq_x_0) = c_Set_Oinsert(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = c_Complete__Lattice_Ocomplete__lattice__class_OSUPR(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( c_COMBB(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = c_COMBB(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( c_COMBC(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = c_COMBC(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( c_COMBI(Eq_x_0) = c_COMBI(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( c_COMBK(Eq_x_0,Eq_x_1,Eq_x_2) = c_COMBK(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( c_COMBS(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = c_COMBS(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( c_Finite__Set_Olinorder__class_OMax(Eq_x_0,Eq_x_1) = c_Finite__Set_Olinorder__class_OMax(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( c_SetInterval_Oord__class_OlessThan(Eq_x_0,Eq_x_1) = c_SetInterval_Oord__class_OlessThan(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( c_Com_Ocom_OCond(Eq_x_0,Eq_x_1,Eq_x_2) = c_Com_Ocom_OCond(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( c_Finite__Set_Ofold1(Eq_x_0,Eq_x_1,Eq_x_2) = c_Finite__Set_Ofold1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( c_Finite__Set_Ofold1Set(Eq_x_0,Eq_x_1,Eq_x_2) = c_Finite__Set_Ofold1Set(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( c_The(Eq_x_0,Eq_x_1) = c_The(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( c_Com_Ocom_OWhile(Eq_x_0,Eq_x_1) = c_Com_Ocom_OWhile(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( c_Complete__Lattice_OInf__class_OInf(Eq_x_0,Eq_x_1) = c_Complete__Lattice_OInf__class_OInf(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( c_Com_Ocom_OSemi(Eq_x_0,Eq_x_1) = c_Com_Ocom_OSemi(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( c_Complete__Lattice_OSup__class_OSup(Eq_x_0,Eq_x_1) = c_Complete__Lattice_OSup__class_OSup(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( c_SetInterval_Oord__class_OatLeastAtMost(Eq_x_0,Eq_x_1,Eq_x_2) = c_SetInterval_Oord__class_OatLeastAtMost(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( c_Finite__Set_Olinorder__class_OMin(Eq_x_0,Eq_x_1) = c_Finite__Set_Olinorder__class_OMin(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( c_fequal(Eq_x_0,Eq_x_1) = c_fequal(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( c_Hoare__Mirabelle_Otriple_Otriple(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = c_Hoare__Mirabelle_Otriple_Otriple(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( c_Hoare__Mirabelle_Otriple_Otriple__case(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = c_Hoare__Mirabelle_Otriple_Otriple__case(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( c_Hoare__Mirabelle_Otriple_Otriple__rec(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = c_Hoare__Mirabelle_Otriple_Otriple__rec(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( tc_Hoare__Mirabelle_Otriple(Eq_x_0) = tc_Hoare__Mirabelle_Otriple(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( c_Hoare__Mirabelle_Opeek__and(Eq_x_0,Eq_x_1,Eq_x_2) = c_Hoare__Mirabelle_Opeek__and(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( c_Nitpick_Osko__Nitpick__XEx1__def__1__3(Eq_x_0,Eq_x_1) = c_Nitpick_Osko__Nitpick__XEx1__def__1__3(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,axiom,
( c_Set_Ocontents(Eq_x_0,Eq_x_1) = c_Set_Ocontents(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( v_sko__Hoare__Mirabelle__Xconseq12__3(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xconseq12__3(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( v_sko__Hoare__Mirabelle__Xconseq12__2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xconseq12__2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_45,axiom,
( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5) = v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__3(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5)
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__2(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_47,axiom,
( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xhoare__derivs__Xintros__6__1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,axiom,
( v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_49,axiom,
( v_sko__Hoare__Mirabelle__Xconseq12__1(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = v_sko__Hoare__Mirabelle__Xconseq12__1(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_50,axiom,
( class_Lattices_Olattice(Eq_y_0)
| ~ class_Lattices_Olattice(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_51,axiom,
( c_Fun_Oinj__on(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ c_Fun_Oinj__on(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_52,axiom,
( class_Lattices_Odistrib__lattice(Eq_y_0)
| ~ class_Lattices_Odistrib__lattice(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_53,axiom,
( hBOOL(Eq_y_0)
| ~ hBOOL(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_54,axiom,
( class_Lattices_Oupper__semilattice(Eq_y_0)
| ~ class_Lattices_Oupper__semilattice(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_55,axiom,
( class_OrderedGroup_Oab__group__add(Eq_y_0)
| ~ class_OrderedGroup_Oab__group__add(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_56,axiom,
( class_Orderings_Olinorder(Eq_y_0)
| ~ class_Orderings_Olinorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_57,axiom,
( c_lessequals(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ c_lessequals(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_58,axiom,
( c_Finite__Set_Ofinite(Eq_y_0,Eq_y_1)
| ~ c_Finite__Set_Ofinite(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( c_Orderings_Olinorder(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ c_Orderings_Olinorder(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( class_Lattices_Olower__semilattice(Eq_y_0)
| ~ class_Lattices_Olower__semilattice(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_61,axiom,
( class_Complete__Lattice_Ocomplete__lattice(Eq_y_0)
| ~ class_Complete__Lattice_Ocomplete__lattice(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_62,axiom,
( c_Finite__Set_Ofun__left__comm__idem(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ c_Finite__Set_Ofun__left__comm__idem(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( class_Orderings_Oorder(Eq_y_0)
| ~ class_Orderings_Oorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_64,axiom,
( class_HOL_Ominus(Eq_y_0)
| ~ class_HOL_Ominus(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( c_Complete__Lattice_Ocomplete__lattice(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4,Eq_y_5,Eq_y_6,Eq_y_7,Eq_y_8)
| ~ c_Complete__Lattice_Ocomplete__lattice(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4,Eq_x_5,Eq_x_6,Eq_x_7,Eq_x_8)
| Eq_x_8 != Eq_y_8
| Eq_x_7 != Eq_y_7
| Eq_x_6 != Eq_y_6
| Eq_x_5 != Eq_y_5
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( class_Finite__Set_Ofinite_Ofinite(Eq_y_0)
| ~ class_Finite__Set_Ofinite_Ofinite(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,axiom,
( class_HOL_Oord(Eq_y_0)
| ~ class_HOL_Oord(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_68,axiom,
( class_Lattices_Obounded__lattice(Eq_y_0)
| ~ class_Lattices_Obounded__lattice(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_69,axiom,
( class_Orderings_Obot(Eq_y_0)
| ~ class_Orderings_Obot(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_70,axiom,
( class_Orderings_Opreorder(Eq_y_0)
| ~ class_Orderings_Opreorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_71,axiom,
( class_OrderedGroup_Opordered__ab__group__add(Eq_y_0)
| ~ class_OrderedGroup_Opordered__ab__group__add(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_72,axiom,
( c_Hoare__Mirabelle_Ohoare__derivs(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV826-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n014.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sun Sep 20 04:47:41 UTC 2026
% 0.09/5.38 % CPUTime :
% 32.94/38.24 % SZS status Unsatisfiable for theBenchmark
% 32.94/38.24 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------