%------------------------------------------------------------------------------ % File : cocATP---0.2.0 % Problem : ITP121^1 : TPTP v7.5.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % DateTime : Sun Mar 21 13:24:14 EDT 2021 % Result : Theorem 124.01s % Output : Proof 124.01s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : ITP121^1 : TPTP v7.5.0. Released v7.5.0. % 0.07/0.12 % Command : python CASC.py /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % DateTime : Fri Mar 19 06:22:37 EDT 2021 % 0.13/0.33 % CPUTime : % 0.13/0.34 ModuleCmd_Load.c(213):ERROR:105: Unable to locate a modulefile for 'python/python27' % 0.13/0.35 Python 2.7.5 % 0.45/0.62 Using paths ['/home/cristobal/cocATP/CASC/TPTP/', '/export/starexec/sandbox/benchmark/', '/export/starexec/sandbox/benchmark/'] % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d440e0>, <kernel.Type object at 0x1d444d0>) of role type named ty_n_t__Set__Oset_Itf__a_J % 0.45/0.62 Using role type % 0.45/0.62 Declaring set_a:Type % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d48518>, <kernel.Type object at 0x1d445f0>) of role type named ty_n_tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring a:Type % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44680>, <kernel.DependentProduct object at 0x1d44cb0>) of role type named sy_c_Conditionally__Complete__Lattices_Opreorder_Obdd__above_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring condit1627435690bove_a:((a->(a->Prop))->(set_a->Prop)) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d443b0>, <kernel.DependentProduct object at 0x1d44f80>) of role type named sy_c_Conditionally__Complete__Lattices_Opreorder_Obdd__below_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring condit1001553558elow_a:((a->(a->Prop))->(set_a->Prop)) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44c20>, <kernel.DependentProduct object at 0x1d449e0>) of role type named sy_c_Finite__Set_Ocomp__fun__idem_001tf__a_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring finite40241356em_a_a:((a->(a->a))->Prop) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44320>, <kernel.DependentProduct object at 0x1d44680>) of role type named sy_c_Finite__Set_Ofinite_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring finite_finite_a:(set_a->Prop) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44f80>, <kernel.DependentProduct object at 0x1d44320>) of role type named sy_c_Groups_Oabel__semigroup_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring abel_semigroup_a:((a->(a->a))->Prop) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x2b41e2abd5f0>, <kernel.DependentProduct object at 0x1d443b0>) of role type named sy_c_Groups_Osemigroup_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring semigroup_a:((a->(a->a))->Prop) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x2b41e2abd5f0>, <kernel.DependentProduct object at 0x1d44c20>) of role type named sy_c_Lattices_Oinf__class_Oinf_001t__Set__Oset_Itf__a_J % 0.45/0.62 Using role type % 0.45/0.62 Declaring inf_inf_set_a:(set_a->(set_a->set_a)) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44830>, <kernel.DependentProduct object at 0x1d44cb0>) of role type named sy_c_Lattices_Osemilattice_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring semilattice_a:((a->(a->a))->Prop) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x2b41dafe07a0>, <kernel.DependentProduct object at 0x1d443b0>) of role type named sy_c_Lattices__Big_Osemilattice__inf_OInf__fin_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring lattic247676691_fin_a:((a->(a->a))->(set_a->a)) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x2b41e2ab68c0>, <kernel.DependentProduct object at 0x1d449e0>) of role type named sy_c_Lattices__Big_Osemilattice__set_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring lattic1885654924_set_a:((a->(a->a))->Prop) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x2b41e2ab68c0>, <kernel.DependentProduct object at 0x1d44f80>) of role type named sy_c_Lattices__Big_Osemilattice__sup_OSup__fin_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring lattic1781219155_fin_a:((a->(a->a))->(set_a->a)) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44cb0>, <kernel.DependentProduct object at 0x1d449e0>) of role type named sy_c_Modular__Distrib__Lattice__Mirabelle__ybbibajlty_Olattice_Oa__aux_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring modula17988509_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44c20>, <kernel.DependentProduct object at 0x1d44fc8>) of role type named sy_c_Modular__Distrib__Lattice__Mirabelle__ybbibajlty_Olattice_Ob__aux_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring modula1373251614_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d44a28>, <kernel.DependentProduct object at 0x1d42560>) of role type named sy_c_Modular__Distrib__Lattice__Mirabelle__ybbibajlty_Olattice_Oc__aux_001tf__a % 0.45/0.62 Using role type % 0.45/0.62 Declaring modula581031071_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))) % 0.45/0.62 FOF formula (<kernel.Constant object at 0x1d449e0>, <kernel.DependentProduct object at 0x1d422d8>) of role type named sy_c_Modular__Distrib__Lattice__Mirabelle__ybbibajlty_Olattice_Od__aux_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring modula1936294176_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d44c20>, <kernel.DependentProduct object at 0x1d42710>) of role type named sy_c_Modular__Distrib__Lattice__Mirabelle__ybbibajlty_Olattice_Oe__aux_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring modula1144073633_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d44a28>, <kernel.DependentProduct object at 0x1d42758>) of role type named sy_c_Modular__Distrib__Lattice__Mirabelle__ybbibajlty_Olattice_Oincomp_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring modula1727524044comp_a:((a->(a->Prop))->(a->(a->Prop))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d44fc8>, <kernel.Constant object at 0x1d42f80>) of role type named sy_c_Orderings_Obot__class_Obot_001t__Set__Oset_Itf__a_J % 0.47/0.63 Using role type % 0.47/0.63 Declaring bot_bot_set_a:set_a % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d44fc8>, <kernel.DependentProduct object at 0x1d425a8>) of role type named sy_c_Orderings_Oord_OLeast_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring least_a:((a->(a->Prop))->((a->Prop)->a)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d44fc8>, <kernel.DependentProduct object at 0x1d42f80>) of role type named sy_c_Orderings_Oord_Omax_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring max_a:((a->(a->Prop))->(a->(a->a))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42758>, <kernel.DependentProduct object at 0x1d42b90>) of role type named sy_c_Orderings_Oord_Omin_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring min_a:((a->(a->Prop))->(a->(a->a))) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42710>, <kernel.DependentProduct object at 0x1d42f38>) of role type named sy_c_Orderings_Oord__class_Oless__eq_001t__Set__Oset_Itf__a_J % 0.47/0.63 Using role type % 0.47/0.63 Declaring ord_less_eq_set_a:(set_a->(set_a->Prop)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42bd8>, <kernel.DependentProduct object at 0x1d42200>) of role type named sy_c_Orderings_Oorder_OGreatest_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring greatest_a:((a->(a->Prop))->((a->Prop)->a)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42758>, <kernel.DependentProduct object at 0x1d42f80>) of role type named sy_c_Orderings_Oorder_Oantimono_001tf__a_001t__Set__Oset_Itf__a_J % 0.47/0.63 Using role type % 0.47/0.63 Declaring antimono_a_set_a:((a->(a->Prop))->((a->set_a)->Prop)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42248>, <kernel.DependentProduct object at 0x1d42998>) of role type named sy_c_Orderings_Oorder_Omono_001tf__a_001t__Set__Oset_Itf__a_J % 0.47/0.63 Using role type % 0.47/0.63 Declaring mono_a_set_a:((a->(a->Prop))->((a->set_a)->Prop)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42b90>, <kernel.DependentProduct object at 0x1d42200>) of role type named sy_c_Set_OCollect_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring collect_a:((a->Prop)->set_a) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d427e8>, <kernel.DependentProduct object at 0x1d42758>) of role type named sy_c_Set_Oinsert_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring insert_a:(a->(set_a->set_a)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42f38>, <kernel.DependentProduct object at 0x1d42f80>) of role type named sy_c_Set__Interval_Oord_OatLeast_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring set_atLeast_a:((a->(a->Prop))->(a->set_a)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42200>, <kernel.DependentProduct object at 0x1d42758>) of role type named sy_c_Set__Interval_Oord_OatMost_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring set_atMost_a:((a->(a->Prop))->(a->set_a)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d427a0>, <kernel.DependentProduct object at 0x1d42d88>) of role type named sy_c_member_001tf__a % 0.47/0.63 Using role type % 0.47/0.63 Declaring member_a:(a->(set_a->Prop)) % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42248>, <kernel.Constant object at 0x1d42d88>) of role type named sy_v_a % 0.47/0.63 Using role type % 0.47/0.63 Declaring a2:a % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42200>, <kernel.Constant object at 0x1d42d88>) of role type named sy_v_b % 0.47/0.63 Using role type % 0.47/0.63 Declaring b:a % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d427a0>, <kernel.Constant object at 0x1d42d88>) of role type named sy_v_c % 0.47/0.63 Using role type % 0.47/0.63 Declaring c:a % 0.47/0.63 FOF formula (<kernel.Constant object at 0x1d42248>, <kernel.DependentProduct object at 0x1d42d40>) of role type named sy_v_inf % 0.47/0.65 Using role type % 0.47/0.65 Declaring inf:(a->(a->a)) % 0.47/0.65 FOF formula (<kernel.Constant object at 0x1d42950>, <kernel.DependentProduct object at 0x1d428c0>) of role type named sy_v_less__eq % 0.47/0.65 Using role type % 0.47/0.65 Declaring less_eq:(a->(a->Prop)) % 0.47/0.65 FOF formula (<kernel.Constant object at 0x1d42d88>, <kernel.DependentProduct object at 0x1d42b00>) of role type named sy_v_sup % 0.47/0.65 Using role type % 0.47/0.65 Declaring sup:(a->(a->a)) % 0.47/0.65 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((inf ((inf A) B)) C)) ((inf A) ((inf B) C)))) of role axiom named fact_0_local_Oinf_Oassoc % 0.47/0.65 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((inf ((inf A) B)) C)) ((inf A) ((inf B) C)))) % 0.47/0.65 FOF formula (forall (A:a) (B:a), (((eq a) ((inf A) B)) ((inf B) A))) of role axiom named fact_1_local_Oinf_Ocommute % 0.47/0.65 A new axiom: (forall (A:a) (B:a), (((eq a) ((inf A) B)) ((inf B) A))) % 0.47/0.65 FOF formula (forall (B:a) (A:a) (C:a), (((eq a) ((inf B) ((inf A) C))) ((inf A) ((inf B) C)))) of role axiom named fact_2_local_Oinf_Oleft__commute % 0.47/0.65 A new axiom: (forall (B:a) (A:a) (C:a), (((eq a) ((inf B) ((inf A) C))) ((inf A) ((inf B) C)))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a) (Z:a), (((eq a) ((inf ((inf X) Y)) Z)) ((inf X) ((inf Y) Z)))) of role axiom named fact_3_local_Oinf__assoc % 0.47/0.65 A new axiom: (forall (X:a) (Y:a) (Z:a), (((eq a) ((inf ((inf X) Y)) Z)) ((inf X) ((inf Y) Z)))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a), (((eq a) ((inf X) Y)) ((inf Y) X))) of role axiom named fact_4_local_Oinf__commute % 0.47/0.65 A new axiom: (forall (X:a) (Y:a), (((eq a) ((inf X) Y)) ((inf Y) X))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a) (Z:a), (((eq a) ((inf X) ((inf Y) Z))) ((inf Y) ((inf X) Z)))) of role axiom named fact_5_local_Oinf__left__commute % 0.47/0.65 A new axiom: (forall (X:a) (Y:a) (Z:a), (((eq a) ((inf X) ((inf Y) Z))) ((inf Y) ((inf X) Z)))) % 0.47/0.65 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((sup ((sup A) B)) C)) ((sup A) ((sup B) C)))) of role axiom named fact_6_local_Osup_Oassoc % 0.47/0.65 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((sup ((sup A) B)) C)) ((sup A) ((sup B) C)))) % 0.47/0.65 FOF formula (forall (A:a) (B:a), (((eq a) ((sup A) B)) ((sup B) A))) of role axiom named fact_7_local_Osup_Ocommute % 0.47/0.65 A new axiom: (forall (A:a) (B:a), (((eq a) ((sup A) B)) ((sup B) A))) % 0.47/0.65 FOF formula (forall (B:a) (A:a) (C:a), (((eq a) ((sup B) ((sup A) C))) ((sup A) ((sup B) C)))) of role axiom named fact_8_local_Osup_Oleft__commute % 0.47/0.65 A new axiom: (forall (B:a) (A:a) (C:a), (((eq a) ((sup B) ((sup A) C))) ((sup A) ((sup B) C)))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a) (Z:a), (((eq a) ((sup ((sup X) Y)) Z)) ((sup X) ((sup Y) Z)))) of role axiom named fact_9_local_Osup__assoc % 0.47/0.65 A new axiom: (forall (X:a) (Y:a) (Z:a), (((eq a) ((sup ((sup X) Y)) Z)) ((sup X) ((sup Y) Z)))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a), (((eq a) ((sup X) Y)) ((sup Y) X))) of role axiom named fact_10_local_Osup__commute % 0.47/0.65 A new axiom: (forall (X:a) (Y:a), (((eq a) ((sup X) Y)) ((sup Y) X))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a) (Z:a), (((eq a) ((sup X) ((sup Y) Z))) ((sup Y) ((sup X) Z)))) of role axiom named fact_11_local_Osup__left__commute % 0.47/0.65 A new axiom: (forall (X:a) (Y:a) (Z:a), (((eq a) ((sup X) ((sup Y) Z))) ((sup Y) ((sup X) Z)))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a) (Z:a), ((forall (X2:a) (Y2:a) (Z2:a), (((eq a) ((inf X2) ((sup Y2) Z2))) ((sup ((inf X2) Y2)) ((inf X2) Z2))))->(((eq a) ((sup X) ((inf Y) Z))) ((inf ((sup X) Y)) ((sup X) Z))))) of role axiom named fact_12_local_Odistrib__imp1 % 0.47/0.65 A new axiom: (forall (X:a) (Y:a) (Z:a), ((forall (X2:a) (Y2:a) (Z2:a), (((eq a) ((inf X2) ((sup Y2) Z2))) ((sup ((inf X2) Y2)) ((inf X2) Z2))))->(((eq a) ((sup X) ((inf Y) Z))) ((inf ((sup X) Y)) ((sup X) Z))))) % 0.47/0.65 FOF formula (forall (X:a) (Y:a) (Z:a), ((forall (X2:a) (Y2:a) (Z2:a), (((eq a) ((sup X2) ((inf Y2) Z2))) ((inf ((sup X2) Y2)) ((sup X2) Z2))))->(((eq a) ((inf X) ((sup Y) Z))) ((sup ((inf X) Y)) ((inf X) Z))))) of role axiom named fact_13_local_Odistrib__imp2 % 0.47/0.65 A new axiom: (forall (X:a) (Y:a) (Z:a), ((forall (X2:a) (Y2:a) (Z2:a), (((eq a) ((sup X2) ((inf Y2) Z2))) ((inf ((sup X2) Y2)) ((sup X2) Z2))))->(((eq a) ((inf X) ((sup Y) Z))) ((sup ((inf X) Y)) ((inf X) Z))))) % 0.47/0.67 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((sup A) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup A) ((inf B) C)))) of role axiom named fact_14_local_Oa__join__d % 0.47/0.67 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((sup A) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup A) ((inf B) C)))) % 0.47/0.67 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((inf A) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf A) B)) ((inf C) A)))) of role axiom named fact_15_a__meet__d % 0.47/0.67 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((inf A) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf A) B)) ((inf C) A)))) % 0.47/0.67 FOF formula (forall (B:a) (A:a) (C:a), (((eq a) ((sup B) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup B) ((inf C) A)))) of role axiom named fact_16_local_Ob__join__d % 0.47/0.67 A new axiom: (forall (B:a) (A:a) (C:a), (((eq a) ((sup B) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup B) ((inf C) A)))) % 0.47/0.67 FOF formula (forall (B:a) (A:a) (C:a), (((eq a) ((inf B) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf B) C)) ((inf A) B)))) of role axiom named fact_17_b__meet__d % 0.47/0.67 A new axiom: (forall (B:a) (A:a) (C:a), (((eq a) ((inf B) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf B) C)) ((inf A) B)))) % 0.47/0.67 FOF formula (forall (C:a) (A:a) (B:a), (((eq a) ((inf C) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf C) A)) ((inf B) C)))) of role axiom named fact_18_c__meet__d % 0.47/0.67 A new axiom: (forall (C:a) (A:a) (B:a), (((eq a) ((inf C) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf C) A)) ((inf B) C)))) % 0.47/0.67 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1936294176_aux_a inf) sup) A) B) C)) ((sup ((sup ((inf A) B)) ((inf B) C))) ((inf C) A)))) of role axiom named fact_19_local_Od__aux__def % 0.47/0.67 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1936294176_aux_a inf) sup) A) B) C)) ((sup ((sup ((inf A) B)) ((inf B) C))) ((inf C) A)))) % 0.47/0.67 FOF formula (forall (B:a) (C:a) (A:a), (((eq a) (((((modula1936294176_aux_a inf) sup) B) C) A)) (((((modula1936294176_aux_a inf) sup) A) B) C))) of role axiom named fact_20_local_Od__b__c__a % 0.47/0.67 A new axiom: (forall (B:a) (C:a) (A:a), (((eq a) (((((modula1936294176_aux_a inf) sup) B) C) A)) (((((modula1936294176_aux_a inf) sup) A) B) C))) % 0.47/0.67 FOF formula (forall (C:a) (A:a) (B:a), (((eq a) (((((modula1936294176_aux_a inf) sup) C) A) B)) (((((modula1936294176_aux_a inf) sup) A) B) C))) of role axiom named fact_21_local_Od__c__a__b % 0.47/0.67 A new axiom: (forall (C:a) (A:a) (B:a), (((eq a) (((((modula1936294176_aux_a inf) sup) C) A) B)) (((((modula1936294176_aux_a inf) sup) A) B) C))) % 0.47/0.67 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) ((inf A) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf A) ((sup B) C)))) of role axiom named fact_22_local_Oa__meet__e % 0.47/0.67 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) ((inf A) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf A) ((sup B) C)))) % 0.47/0.67 FOF formula (forall (B:a) (A:a) (C:a), (((eq a) ((inf B) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf B) ((sup C) A)))) of role axiom named fact_23_local_Ob__meet__e % 0.47/0.67 A new axiom: (forall (B:a) (A:a) (C:a), (((eq a) ((inf B) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf B) ((sup C) A)))) % 0.47/0.67 FOF formula (forall (C:a) (A:a) (B:a), (((eq a) ((inf C) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf C) ((sup A) B)))) of role axiom named fact_24_local_Oc__meet__e % 0.47/0.67 A new axiom: (forall (C:a) (A:a) (B:a), (((eq a) ((inf C) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf C) ((sup A) B)))) % 0.47/0.67 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1144073633_aux_a inf) sup) A) B) C)) ((inf ((inf ((sup A) B)) ((sup B) C))) ((sup C) A)))) of role axiom named fact_25_local_Oe__aux__def % 0.47/0.67 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1144073633_aux_a inf) sup) A) B) C)) ((inf ((inf ((sup A) B)) ((sup B) C))) ((sup C) A)))) % 0.47/0.67 FOF formula (forall (B:a) (C:a) (A:a), (((eq a) (((((modula1144073633_aux_a inf) sup) B) C) A)) (((((modula1144073633_aux_a inf) sup) A) B) C))) of role axiom named fact_26_local_Oe__b__c__a % 0.47/0.67 A new axiom: (forall (B:a) (C:a) (A:a), (((eq a) (((((modula1144073633_aux_a inf) sup) B) C) A)) (((((modula1144073633_aux_a inf) sup) A) B) C))) % 0.47/0.68 FOF formula (forall (C:a) (A:a) (B:a), (((eq a) (((((modula1144073633_aux_a inf) sup) C) A) B)) (((((modula1144073633_aux_a inf) sup) A) B) C))) of role axiom named fact_27_local_Oe__c__a__b % 0.47/0.68 A new axiom: (forall (C:a) (A:a) (B:a), (((eq a) (((((modula1144073633_aux_a inf) sup) C) A) B)) (((((modula1144073633_aux_a inf) sup) A) B) C))) % 0.47/0.68 FOF formula (forall (A:a), (((eq a) ((inf A) A)) A)) of role axiom named fact_28_local_Oinf_Oidem % 0.47/0.68 A new axiom: (forall (A:a), (((eq a) ((inf A) A)) A)) % 0.47/0.68 FOF formula (forall (A:a) (B:a), (((eq a) ((inf A) ((inf A) B))) ((inf A) B))) of role axiom named fact_29_local_Oinf_Oleft__idem % 0.47/0.68 A new axiom: (forall (A:a) (B:a), (((eq a) ((inf A) ((inf A) B))) ((inf A) B))) % 0.47/0.68 FOF formula (forall (A:a) (B:a), (((eq a) ((inf ((inf A) B)) B)) ((inf A) B))) of role axiom named fact_30_local_Oinf_Oright__idem % 0.47/0.68 A new axiom: (forall (A:a) (B:a), (((eq a) ((inf ((inf A) B)) B)) ((inf A) B))) % 0.47/0.68 FOF formula (forall (X:a), (((eq a) ((inf X) X)) X)) of role axiom named fact_31_local_Oinf__idem % 0.47/0.68 A new axiom: (forall (X:a), (((eq a) ((inf X) X)) X)) % 0.47/0.68 FOF formula (forall (X:a) (Y:a), (((eq a) ((inf X) ((inf X) Y))) ((inf X) Y))) of role axiom named fact_32_local_Oinf__left__idem % 0.47/0.68 A new axiom: (forall (X:a) (Y:a), (((eq a) ((inf X) ((inf X) Y))) ((inf X) Y))) % 0.47/0.68 FOF formula (forall (X:a) (Y:a), (((eq a) ((inf ((inf X) Y)) Y)) ((inf X) Y))) of role axiom named fact_33_local_Oinf__right__idem % 0.47/0.68 A new axiom: (forall (X:a) (Y:a), (((eq a) ((inf ((inf X) Y)) Y)) ((inf X) Y))) % 0.47/0.68 FOF formula (forall (A:a), (((eq a) ((sup A) A)) A)) of role axiom named fact_34_local_Osup_Oidem % 0.47/0.68 A new axiom: (forall (A:a), (((eq a) ((sup A) A)) A)) % 0.47/0.68 FOF formula (forall (A:a) (B:a), (((eq a) ((sup A) ((sup A) B))) ((sup A) B))) of role axiom named fact_35_local_Osup_Oleft__idem % 0.47/0.68 A new axiom: (forall (A:a) (B:a), (((eq a) ((sup A) ((sup A) B))) ((sup A) B))) % 0.47/0.68 FOF formula (forall (A:a) (B:a), (((eq a) ((sup ((sup A) B)) B)) ((sup A) B))) of role axiom named fact_36_local_Osup_Oright__idem % 0.47/0.68 A new axiom: (forall (A:a) (B:a), (((eq a) ((sup ((sup A) B)) B)) ((sup A) B))) % 0.47/0.68 FOF formula (forall (X:a), (((eq a) ((sup X) X)) X)) of role axiom named fact_37_local_Osup__idem % 0.47/0.68 A new axiom: (forall (X:a), (((eq a) ((sup X) X)) X)) % 0.47/0.68 FOF formula (forall (X:a) (Y:a), (((eq a) ((sup X) ((sup X) Y))) ((sup X) Y))) of role axiom named fact_38_local_Osup__left__idem % 0.47/0.68 A new axiom: (forall (X:a) (Y:a), (((eq a) ((sup X) ((sup X) Y))) ((sup X) Y))) % 0.47/0.68 FOF formula (((eq a) ((sup ((inf ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)))) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) of role axiom named fact_39_calculation % 0.47/0.68 A new axiom: (((eq a) ((sup ((inf ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)))) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 0.47/0.68 FOF formula (forall (X:a) (Y:a), (((eq a) ((inf X) ((sup X) Y))) X)) of role axiom named fact_40_local_Oinf__sup__absorb % 0.47/0.68 A new axiom: (forall (X:a) (Y:a), (((eq a) ((inf X) ((sup X) Y))) X)) % 0.47/0.68 FOF formula (forall (X:a) (Y:a), (((eq a) ((sup X) ((inf X) Y))) X)) of role axiom named fact_41_local_Osup__inf__absorb % 0.47/0.68 A new axiom: (forall (X:a) (Y:a), (((eq a) ((sup X) ((inf X) Y))) X)) % 0.47/0.68 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) ((sup ((inf B) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) of role axiom named fact_42_local_Ob__aux__def % 0.47/0.69 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) ((sup ((inf B) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) % 0.47/0.69 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) ((sup ((inf C) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) of role axiom named fact_43_local_Oc__aux__def % 0.47/0.69 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) ((sup ((inf C) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) % 0.47/0.69 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula17988509_aux_a inf) sup) A) B) C)) ((sup ((inf A) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) of role axiom named fact_44_local_Oa__aux__def % 0.47/0.69 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula17988509_aux_a inf) sup) A) B) C)) ((sup ((inf A) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) % 0.47/0.69 FOF formula (forall (A:a) (P:(a->Prop)), (((eq Prop) ((member_a A) (collect_a P))) (P A))) of role axiom named fact_45_mem__Collect__eq % 0.47/0.69 A new axiom: (forall (A:a) (P:(a->Prop)), (((eq Prop) ((member_a A) (collect_a P))) (P A))) % 0.47/0.69 FOF formula (forall (A2:set_a), (((eq set_a) (collect_a (fun (X3:a)=> ((member_a X3) A2)))) A2)) of role axiom named fact_46_Collect__mem__eq % 0.47/0.69 A new axiom: (forall (A2:set_a), (((eq set_a) (collect_a (fun (X3:a)=> ((member_a X3) A2)))) A2)) % 0.47/0.69 FOF formula (forall (P:(a->Prop)) (Q:(a->Prop)), ((forall (X2:a), (((eq Prop) (P X2)) (Q X2)))->(((eq set_a) (collect_a P)) (collect_a Q)))) of role axiom named fact_47_Collect__cong % 0.47/0.69 A new axiom: (forall (P:(a->Prop)) (Q:(a->Prop)), ((forall (X2:a), (((eq Prop) (P X2)) (Q X2)))->(((eq set_a) (collect_a P)) (collect_a Q)))) % 0.47/0.69 FOF formula (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1936294176_aux_a) modula1936294176_aux_a) of role axiom named fact_48_lattice_Od__aux_Ocong % 0.47/0.69 A new axiom: (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1936294176_aux_a) modula1936294176_aux_a) % 0.47/0.69 FOF formula (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1144073633_aux_a) modula1144073633_aux_a) of role axiom named fact_49_lattice_Oe__aux_Ocong % 0.47/0.69 A new axiom: (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1144073633_aux_a) modula1144073633_aux_a) % 0.47/0.69 FOF formula ((less_eq (((((modula1936294176_aux_a inf) sup) a2) b) c)) (((((modula1144073633_aux_a inf) sup) a2) b) c)) of role axiom named fact_50_d__less__e % 0.47/0.69 A new axiom: ((less_eq (((((modula1936294176_aux_a inf) sup) a2) b) c)) (((((modula1144073633_aux_a inf) sup) a2) b) c)) % 0.47/0.69 FOF formula (finite40241356em_a_a sup) of role axiom named fact_51_local_Ocomp__fun__idem__sup % 0.47/0.69 A new axiom: (finite40241356em_a_a sup) % 0.47/0.69 FOF formula (finite40241356em_a_a inf) of role axiom named fact_52_local_Ocomp__fun__idem__inf % 0.47/0.69 A new axiom: (finite40241356em_a_a inf) % 0.47/0.69 FOF formula (semigroup_a sup) of role axiom named fact_53_local_Osup_Osemigroup__axioms % 0.47/0.69 A new axiom: (semigroup_a sup) % 0.47/0.69 FOF formula (semigroup_a inf) of role axiom named fact_54_local_Oinf_Osemigroup__axioms % 0.47/0.69 A new axiom: (semigroup_a inf) % 0.47/0.69 FOF formula (semilattice_a sup) of role axiom named fact_55_local_Osup_Osemilattice__axioms % 0.47/0.69 A new axiom: (semilattice_a sup) % 0.47/0.69 FOF formula (semilattice_a inf) of role axiom named fact_56_local_Oinf_Osemilattice__axioms % 0.47/0.69 A new axiom: (semilattice_a inf) % 0.47/0.69 FOF formula (abel_semigroup_a sup) of role axiom named fact_57_local_Osup_Oabel__semigroup__axioms % 0.47/0.69 A new axiom: (abel_semigroup_a sup) % 0.47/0.69 FOF formula (abel_semigroup_a inf) of role axiom named fact_58_local_Oinf_Oabel__semigroup__axioms % 0.47/0.69 A new axiom: (abel_semigroup_a inf) % 0.47/0.69 FOF formula (lattic1885654924_set_a sup) of role axiom named fact_59_local_OSup__fin_Osemilattice__set__axioms % 0.47/0.69 A new axiom: (lattic1885654924_set_a sup) % 0.47/0.69 FOF formula (lattic1885654924_set_a inf) of role axiom named fact_60_local_OInf__fin_Osemilattice__set__axioms % 0.55/0.71 A new axiom: (lattic1885654924_set_a inf) % 0.55/0.71 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) B) C) A))) of role axiom named fact_61_local_Ob__a % 0.55/0.71 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) B) C) A))) % 0.55/0.71 FOF formula (forall (X:a) (Y:a), (((less_eq X) Y)->(((less_eq Y) X)->(((eq a) X) Y)))) of role axiom named fact_62_local_Oantisym % 0.55/0.71 A new axiom: (forall (X:a) (Y:a), (((less_eq X) Y)->(((less_eq Y) X)->(((eq a) X) Y)))) % 0.55/0.71 FOF formula (forall (Y:a) (X:a), (((less_eq Y) X)->(((eq Prop) ((less_eq X) Y)) (((eq a) X) Y)))) of role axiom named fact_63_local_Oantisym__conv % 0.55/0.71 A new axiom: (forall (Y:a) (X:a), (((less_eq Y) X)->(((eq Prop) ((less_eq X) Y)) (((eq a) X) Y)))) % 0.55/0.71 FOF formula (forall (B:a) (A:a), (((less_eq B) A)->(((less_eq A) B)->(((eq a) A) B)))) of role axiom named fact_64_local_Odual__order_Oantisym % 0.55/0.71 A new axiom: (forall (B:a) (A:a), (((less_eq B) A)->(((less_eq A) B)->(((eq a) A) B)))) % 0.55/0.71 FOF formula (((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (A3:a) (B2:a)=> ((and ((less_eq B2) A3)) ((less_eq A3) B2)))) of role axiom named fact_65_local_Odual__order_Oeq__iff % 0.55/0.71 A new axiom: (((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (A3:a) (B2:a)=> ((and ((less_eq B2) A3)) ((less_eq A3) B2)))) % 0.55/0.71 FOF formula (forall (B:a) (A:a) (C:a), (((less_eq B) A)->(((less_eq C) B)->((less_eq C) A)))) of role axiom named fact_66_local_Odual__order_Otrans % 0.55/0.71 A new axiom: (forall (B:a) (A:a) (C:a), (((less_eq B) A)->(((less_eq C) B)->((less_eq C) A)))) % 0.55/0.71 FOF formula (((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (X3:a) (Y4:a)=> ((and ((less_eq X3) Y4)) ((less_eq Y4) X3)))) of role axiom named fact_67_local_Oeq__iff % 0.55/0.71 A new axiom: (((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (X3:a) (Y4:a)=> ((and ((less_eq X3) Y4)) ((less_eq Y4) X3)))) % 0.55/0.71 FOF formula (forall (X:a) (Y:a), ((((eq a) X) Y)->((less_eq X) Y))) of role axiom named fact_68_local_Oeq__refl % 0.55/0.71 A new axiom: (forall (X:a) (Y:a), ((((eq a) X) Y)->((less_eq X) Y))) % 0.55/0.71 FOF formula (forall (A:a) (B:a) (C:a), ((((eq a) A) B)->(((less_eq B) C)->((less_eq A) C)))) of role axiom named fact_69_local_Oord__eq__le__trans % 0.55/0.71 A new axiom: (forall (A:a) (B:a) (C:a), ((((eq a) A) B)->(((less_eq B) C)->((less_eq A) C)))) % 0.55/0.71 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq A) B)->((((eq a) B) C)->((less_eq A) C)))) of role axiom named fact_70_local_Oord__le__eq__trans % 0.55/0.71 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq A) B)->((((eq a) B) C)->((less_eq A) C)))) % 0.55/0.71 FOF formula (forall (A:a) (B:a), (((less_eq A) B)->(((less_eq B) A)->(((eq a) A) B)))) of role axiom named fact_71_local_Oorder_Oantisym % 0.55/0.71 A new axiom: (forall (A:a) (B:a), (((less_eq A) B)->(((less_eq B) A)->(((eq a) A) B)))) % 0.55/0.71 FOF formula (((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (A3:a) (B2:a)=> ((and ((less_eq A3) B2)) ((less_eq B2) A3)))) of role axiom named fact_72_local_Oorder_Oeq__iff % 0.55/0.71 A new axiom: (((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (A3:a) (B2:a)=> ((and ((less_eq A3) B2)) ((less_eq B2) A3)))) % 0.55/0.71 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq A) B)->(((less_eq B) C)->((less_eq A) C)))) of role axiom named fact_73_local_Oorder_Otrans % 0.55/0.71 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq A) B)->(((less_eq B) C)->((less_eq A) C)))) % 0.55/0.71 FOF formula (forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((less_eq Y) Z)->((less_eq X) Z)))) of role axiom named fact_74_local_Oorder__trans % 0.55/0.71 A new axiom: (forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((less_eq Y) Z)->((less_eq X) Z)))) % 0.55/0.71 FOF formula (forall (B:a) (X:a) (A:a), (((less_eq B) X)->((less_eq ((inf A) B)) X))) of role axiom named fact_75_local_Ole__infI2 % 0.55/0.71 A new axiom: (forall (B:a) (X:a) (A:a), (((less_eq B) X)->((less_eq ((inf A) B)) X))) % 0.55/0.71 FOF formula (forall (A:a) (X:a) (B:a), (((less_eq A) X)->((less_eq ((inf A) B)) X))) of role axiom named fact_76_local_Ole__infI1 % 0.55/0.71 A new axiom: (forall (A:a) (X:a) (B:a), (((less_eq A) X)->((less_eq ((inf A) B)) X))) % 0.55/0.73 FOF formula (forall (X:a) (A:a) (B:a), (((less_eq X) A)->(((less_eq X) B)->((less_eq X) ((inf A) B))))) of role axiom named fact_77_local_Ole__infI % 0.55/0.73 A new axiom: (forall (X:a) (A:a) (B:a), (((less_eq X) A)->(((less_eq X) B)->((less_eq X) ((inf A) B))))) % 0.55/0.73 FOF formula (forall (X:a) (A:a) (B:a), (((less_eq X) ((inf A) B))->((((less_eq X) A)->(((less_eq X) B)->False))->False))) of role axiom named fact_78_local_Ole__infE % 0.55/0.73 A new axiom: (forall (X:a) (A:a) (B:a), (((less_eq X) ((inf A) B))->((((less_eq X) A)->(((less_eq X) B)->False))->False))) % 0.55/0.73 FOF formula (forall (X:a) (Y:a), (((eq Prop) ((less_eq X) Y)) (((eq a) ((inf X) Y)) X))) of role axiom named fact_79_local_Ole__iff__inf % 0.55/0.73 A new axiom: (forall (X:a) (Y:a), (((eq Prop) ((less_eq X) Y)) (((eq a) ((inf X) Y)) X))) % 0.55/0.73 FOF formula (forall (F:(a->(a->a))) (X:a) (Y:a), ((forall (X2:a) (Y2:a), ((less_eq ((F X2) Y2)) X2))->((forall (X2:a) (Y2:a), ((less_eq ((F X2) Y2)) Y2))->((forall (X2:a) (Y2:a) (Z2:a), (((less_eq X2) Y2)->(((less_eq X2) Z2)->((less_eq X2) ((F Y2) Z2)))))->(((eq a) ((inf X) Y)) ((F X) Y)))))) of role axiom named fact_80_local_Oinf__unique % 0.55/0.73 A new axiom: (forall (F:(a->(a->a))) (X:a) (Y:a), ((forall (X2:a) (Y2:a), ((less_eq ((F X2) Y2)) X2))->((forall (X2:a) (Y2:a), ((less_eq ((F X2) Y2)) Y2))->((forall (X2:a) (Y2:a) (Z2:a), (((less_eq X2) Y2)->(((less_eq X2) Z2)->((less_eq X2) ((F Y2) Z2)))))->(((eq a) ((inf X) Y)) ((F X) Y)))))) % 0.55/0.73 FOF formula (forall (A:a) (C:a) (B:a) (D:a), (((less_eq A) C)->(((less_eq B) D)->((less_eq ((inf A) B)) ((inf C) D))))) of role axiom named fact_81_local_Oinf__mono % 0.55/0.73 A new axiom: (forall (A:a) (C:a) (B:a) (D:a), (((less_eq A) C)->(((less_eq B) D)->((less_eq ((inf A) B)) ((inf C) D))))) % 0.55/0.73 FOF formula (forall (X:a) (Y:a), ((less_eq ((inf X) Y)) Y)) of role axiom named fact_82_local_Oinf__le2 % 0.55/0.73 A new axiom: (forall (X:a) (Y:a), ((less_eq ((inf X) Y)) Y)) % 0.55/0.73 FOF formula (forall (X:a) (Y:a), ((less_eq ((inf X) Y)) X)) of role axiom named fact_83_local_Oinf__le1 % 0.55/0.73 A new axiom: (forall (X:a) (Y:a), ((less_eq ((inf X) Y)) X)) % 0.55/0.73 FOF formula (forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((less_eq X) Z)->((less_eq X) ((inf Y) Z))))) of role axiom named fact_84_local_Oinf__greatest % 0.55/0.73 A new axiom: (forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((less_eq X) Z)->((less_eq X) ((inf Y) Z))))) % 0.55/0.73 FOF formula (forall (Y:a) (X:a), (((less_eq Y) X)->(((eq a) ((inf X) Y)) Y))) of role axiom named fact_85_local_Oinf__absorb2 % 0.55/0.73 A new axiom: (forall (Y:a) (X:a), (((less_eq Y) X)->(((eq a) ((inf X) Y)) Y))) % 0.55/0.73 FOF formula (forall (X:a) (Y:a), (((less_eq X) Y)->(((eq a) ((inf X) Y)) X))) of role axiom named fact_86_local_Oinf__absorb1 % 0.55/0.73 A new axiom: (forall (X:a) (Y:a), (((less_eq X) Y)->(((eq a) ((inf X) Y)) X))) % 0.55/0.73 FOF formula (forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) A) ((inf A) B)))) of role axiom named fact_87_local_Oinf_Oorder__iff % 0.55/0.73 A new axiom: (forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) A) ((inf A) B)))) % 0.55/0.73 FOF formula (forall (A:a) (B:a), ((((eq a) A) ((inf A) B))->((less_eq A) B))) of role axiom named fact_88_local_Oinf_OorderI % 0.55/0.73 A new axiom: (forall (A:a) (B:a), ((((eq a) A) ((inf A) B))->((less_eq A) B))) % 0.55/0.73 FOF formula (forall (A:a) (B:a), (((less_eq A) B)->(((eq a) A) ((inf A) B)))) of role axiom named fact_89_local_Oinf_OorderE % 0.55/0.73 A new axiom: (forall (A:a) (B:a), (((less_eq A) B)->(((eq a) A) ((inf A) B)))) % 0.55/0.73 FOF formula (forall (B:a) (C:a) (A:a), (((less_eq B) C)->((less_eq ((inf A) B)) C))) of role axiom named fact_90_local_Oinf_OcoboundedI2 % 0.55/0.73 A new axiom: (forall (B:a) (C:a) (A:a), (((less_eq B) C)->((less_eq ((inf A) B)) C))) % 0.55/0.73 FOF formula (forall (A:a) (C:a) (B:a), (((less_eq A) C)->((less_eq ((inf A) B)) C))) of role axiom named fact_91_local_Oinf_OcoboundedI1 % 0.55/0.73 A new axiom: (forall (A:a) (C:a) (B:a), (((less_eq A) C)->((less_eq ((inf A) B)) C))) % 0.55/0.73 FOF formula (forall (A:a) (B:a), ((less_eq ((inf A) B)) B)) of role axiom named fact_92_local_Oinf_Ocobounded2 % 0.55/0.73 A new axiom: (forall (A:a) (B:a), ((less_eq ((inf A) B)) B)) % 0.55/0.73 FOF formula (forall (A:a) (B:a), ((less_eq ((inf A) B)) A)) of role axiom named fact_93_local_Oinf_Ocobounded1 % 0.55/0.75 A new axiom: (forall (A:a) (B:a), ((less_eq ((inf A) B)) A)) % 0.55/0.75 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq A) B)->(((less_eq A) C)->((less_eq A) ((inf B) C))))) of role axiom named fact_94_local_Oinf_OboundedI % 0.55/0.75 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq A) B)->(((less_eq A) C)->((less_eq A) ((inf B) C))))) % 0.55/0.75 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq A) ((inf B) C))->((((less_eq A) B)->(((less_eq A) C)->False))->False))) of role axiom named fact_95_local_Oinf_OboundedE % 0.55/0.75 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq A) ((inf B) C))->((((less_eq A) B)->(((less_eq A) C)->False))->False))) % 0.55/0.75 FOF formula (forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) ((inf A) B)) B))) of role axiom named fact_96_local_Oinf_Oabsorb__iff2 % 0.55/0.75 A new axiom: (forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) ((inf A) B)) B))) % 0.55/0.75 FOF formula (forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) ((inf A) B)) A))) of role axiom named fact_97_local_Oinf_Oabsorb__iff1 % 0.55/0.75 A new axiom: (forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) ((inf A) B)) A))) % 0.55/0.75 FOF formula (forall (B:a) (A:a), (((less_eq B) A)->(((eq a) ((inf A) B)) B))) of role axiom named fact_98_local_Oinf_Oabsorb2 % 0.55/0.75 A new axiom: (forall (B:a) (A:a), (((less_eq B) A)->(((eq a) ((inf A) B)) B))) % 0.55/0.75 FOF formula (forall (A:a) (B:a), (((less_eq A) B)->(((eq a) ((inf A) B)) A))) of role axiom named fact_99_local_Oinf_Oabsorb1 % 0.55/0.75 A new axiom: (forall (A:a) (B:a), (((less_eq A) B)->(((eq a) ((inf A) B)) A))) % 0.55/0.75 FOF formula (forall (F:(a->(a->a))) (X:a) (Y:a), ((forall (X2:a) (Y2:a), ((less_eq X2) ((F X2) Y2)))->((forall (X2:a) (Y2:a), ((less_eq Y2) ((F X2) Y2)))->((forall (X2:a) (Y2:a) (Z2:a), (((less_eq Y2) X2)->(((less_eq Z2) X2)->((less_eq ((F Y2) Z2)) X2))))->(((eq a) ((sup X) Y)) ((F X) Y)))))) of role axiom named fact_100_local_Osup__unique % 0.55/0.75 A new axiom: (forall (F:(a->(a->a))) (X:a) (Y:a), ((forall (X2:a) (Y2:a), ((less_eq X2) ((F X2) Y2)))->((forall (X2:a) (Y2:a), ((less_eq Y2) ((F X2) Y2)))->((forall (X2:a) (Y2:a) (Z2:a), (((less_eq Y2) X2)->(((less_eq Z2) X2)->((less_eq ((F Y2) Z2)) X2))))->(((eq a) ((sup X) Y)) ((F X) Y)))))) % 0.55/0.75 FOF formula (forall (A:a) (C:a) (B:a) (D:a), (((less_eq A) C)->(((less_eq B) D)->((less_eq ((sup A) B)) ((sup C) D))))) of role axiom named fact_101_local_Osup__mono % 0.55/0.75 A new axiom: (forall (A:a) (C:a) (B:a) (D:a), (((less_eq A) C)->(((less_eq B) D)->((less_eq ((sup A) B)) ((sup C) D))))) % 0.55/0.75 FOF formula (forall (Y:a) (X:a) (Z:a), (((less_eq Y) X)->(((less_eq Z) X)->((less_eq ((sup Y) Z)) X)))) of role axiom named fact_102_local_Osup__least % 0.55/0.75 A new axiom: (forall (Y:a) (X:a) (Z:a), (((less_eq Y) X)->(((less_eq Z) X)->((less_eq ((sup Y) Z)) X)))) % 0.55/0.75 FOF formula (forall (Y:a) (X:a), ((less_eq Y) ((sup X) Y))) of role axiom named fact_103_local_Osup__ge2 % 0.55/0.75 A new axiom: (forall (Y:a) (X:a), ((less_eq Y) ((sup X) Y))) % 0.55/0.75 FOF formula (forall (X:a) (Y:a), ((less_eq X) ((sup X) Y))) of role axiom named fact_104_local_Osup__ge1 % 0.55/0.75 A new axiom: (forall (X:a) (Y:a), ((less_eq X) ((sup X) Y))) % 0.55/0.75 FOF formula (forall (X:a) (Y:a), (((less_eq X) Y)->(((eq a) ((sup X) Y)) Y))) of role axiom named fact_105_local_Osup__absorb2 % 0.55/0.75 A new axiom: (forall (X:a) (Y:a), (((less_eq X) Y)->(((eq a) ((sup X) Y)) Y))) % 0.55/0.75 FOF formula (forall (Y:a) (X:a), (((less_eq Y) X)->(((eq a) ((sup X) Y)) X))) of role axiom named fact_106_local_Osup__absorb1 % 0.55/0.75 A new axiom: (forall (Y:a) (X:a), (((less_eq Y) X)->(((eq a) ((sup X) Y)) X))) % 0.55/0.75 FOF formula (forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) A) ((sup A) B)))) of role axiom named fact_107_local_Osup_Oorder__iff % 0.55/0.75 A new axiom: (forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) A) ((sup A) B)))) % 0.55/0.75 FOF formula (forall (A:a) (B:a), ((((eq a) A) ((sup A) B))->((less_eq B) A))) of role axiom named fact_108_local_Osup_OorderI % 0.55/0.75 A new axiom: (forall (A:a) (B:a), ((((eq a) A) ((sup A) B))->((less_eq B) A))) % 0.55/0.75 FOF formula (forall (B:a) (A:a), (((less_eq B) A)->(((eq a) A) ((sup A) B)))) of role axiom named fact_109_local_Osup_OorderE % 0.55/0.75 A new axiom: (forall (B:a) (A:a), (((less_eq B) A)->(((eq a) A) ((sup A) B)))) % 0.55/0.75 FOF formula (forall (C:a) (A:a) (D:a) (B:a), (((less_eq C) A)->(((less_eq D) B)->((less_eq ((sup C) D)) ((sup A) B))))) of role axiom named fact_110_local_Osup_Omono % 0.61/0.77 A new axiom: (forall (C:a) (A:a) (D:a) (B:a), (((less_eq C) A)->(((less_eq D) B)->((less_eq ((sup C) D)) ((sup A) B))))) % 0.61/0.77 FOF formula (forall (C:a) (B:a) (A:a), (((less_eq C) B)->((less_eq C) ((sup A) B)))) of role axiom named fact_111_local_Osup_OcoboundedI2 % 0.61/0.77 A new axiom: (forall (C:a) (B:a) (A:a), (((less_eq C) B)->((less_eq C) ((sup A) B)))) % 0.61/0.77 FOF formula (forall (C:a) (A:a) (B:a), (((less_eq C) A)->((less_eq C) ((sup A) B)))) of role axiom named fact_112_local_Osup_OcoboundedI1 % 0.61/0.77 A new axiom: (forall (C:a) (A:a) (B:a), (((less_eq C) A)->((less_eq C) ((sup A) B)))) % 0.61/0.77 FOF formula (forall (B:a) (A:a), ((less_eq B) ((sup A) B))) of role axiom named fact_113_local_Osup_Ocobounded2 % 0.61/0.77 A new axiom: (forall (B:a) (A:a), ((less_eq B) ((sup A) B))) % 0.61/0.77 FOF formula (forall (A:a) (B:a), ((less_eq A) ((sup A) B))) of role axiom named fact_114_local_Osup_Ocobounded1 % 0.61/0.77 A new axiom: (forall (A:a) (B:a), ((less_eq A) ((sup A) B))) % 0.61/0.77 FOF formula (forall (B:a) (A:a) (C:a), (((less_eq B) A)->(((less_eq C) A)->((less_eq ((sup B) C)) A)))) of role axiom named fact_115_local_Osup_OboundedI % 0.61/0.77 A new axiom: (forall (B:a) (A:a) (C:a), (((less_eq B) A)->(((less_eq C) A)->((less_eq ((sup B) C)) A)))) % 0.61/0.77 FOF formula (forall (B:a) (C:a) (A:a), (((less_eq ((sup B) C)) A)->((((less_eq B) A)->(((less_eq C) A)->False))->False))) of role axiom named fact_116_local_Osup_OboundedE % 0.61/0.77 A new axiom: (forall (B:a) (C:a) (A:a), (((less_eq ((sup B) C)) A)->((((less_eq B) A)->(((less_eq C) A)->False))->False))) % 0.61/0.77 FOF formula (forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) ((sup A) B)) B))) of role axiom named fact_117_local_Osup_Oabsorb__iff2 % 0.61/0.77 A new axiom: (forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) ((sup A) B)) B))) % 0.61/0.77 FOF formula (forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) ((sup A) B)) A))) of role axiom named fact_118_local_Osup_Oabsorb__iff1 % 0.61/0.77 A new axiom: (forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) ((sup A) B)) A))) % 0.61/0.77 FOF formula (forall (A:a) (B:a), (((less_eq A) B)->(((eq a) ((sup A) B)) B))) of role axiom named fact_119_local_Osup_Oabsorb2 % 0.61/0.77 A new axiom: (forall (A:a) (B:a), (((less_eq A) B)->(((eq a) ((sup A) B)) B))) % 0.61/0.77 FOF formula (forall (B:a) (A:a), (((less_eq B) A)->(((eq a) ((sup A) B)) A))) of role axiom named fact_120_local_Osup_Oabsorb1 % 0.61/0.77 A new axiom: (forall (B:a) (A:a), (((less_eq B) A)->(((eq a) ((sup A) B)) A))) % 0.61/0.77 FOF formula (forall (X:a) (B:a) (A:a), (((less_eq X) B)->((less_eq X) ((sup A) B)))) of role axiom named fact_121_local_Ole__supI2 % 0.61/0.77 A new axiom: (forall (X:a) (B:a) (A:a), (((less_eq X) B)->((less_eq X) ((sup A) B)))) % 0.61/0.77 FOF formula (forall (X:a) (A:a) (B:a), (((less_eq X) A)->((less_eq X) ((sup A) B)))) of role axiom named fact_122_local_Ole__supI1 % 0.61/0.77 A new axiom: (forall (X:a) (A:a) (B:a), (((less_eq X) A)->((less_eq X) ((sup A) B)))) % 0.61/0.77 FOF formula (forall (A:a) (X:a) (B:a), (((less_eq A) X)->(((less_eq B) X)->((less_eq ((sup A) B)) X)))) of role axiom named fact_123_local_Ole__supI % 0.61/0.77 A new axiom: (forall (A:a) (X:a) (B:a), (((less_eq A) X)->(((less_eq B) X)->((less_eq ((sup A) B)) X)))) % 0.61/0.77 FOF formula (forall (A:a) (B:a) (X:a), (((less_eq ((sup A) B)) X)->((((less_eq A) X)->(((less_eq B) X)->False))->False))) of role axiom named fact_124_local_Ole__supE % 0.61/0.77 A new axiom: (forall (A:a) (B:a) (X:a), (((less_eq ((sup A) B)) X)->((((less_eq A) X)->(((less_eq B) X)->False))->False))) % 0.61/0.77 FOF formula (forall (X:a) (Y:a), (((eq Prop) ((less_eq X) Y)) (((eq a) ((sup X) Y)) Y))) of role axiom named fact_125_local_Ole__iff__sup % 0.61/0.77 A new axiom: (forall (X:a) (Y:a), (((eq Prop) ((less_eq X) Y)) (((eq a) ((sup X) Y)) Y))) % 0.61/0.77 FOF formula (forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((eq a) ((sup X) ((inf Y) Z))) ((inf Y) ((sup X) Z))))) of role axiom named fact_126_local_Omodular % 0.61/0.77 A new axiom: (forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((eq a) ((sup X) ((inf Y) Z))) ((inf Y) ((sup X) Z))))) % 0.61/0.77 FOF formula (forall (X:a) (Y:a) (Z:a), ((less_eq ((sup X) ((inf Y) Z))) ((inf ((sup X) Y)) ((sup X) Z)))) of role axiom named fact_127_local_Odistrib__sup__le % 0.61/0.79 A new axiom: (forall (X:a) (Y:a) (Z:a), ((less_eq ((sup X) ((inf Y) Z))) ((inf ((sup X) Y)) ((sup X) Z)))) % 0.61/0.79 FOF formula (forall (X:a) (Y:a) (Z:a), ((less_eq ((sup ((inf X) Y)) ((inf X) Z))) ((inf X) ((sup Y) Z)))) of role axiom named fact_128_local_Odistrib__inf__le % 0.61/0.79 A new axiom: (forall (X:a) (Y:a) (Z:a), ((less_eq ((sup ((inf X) Y)) ((inf X) Z))) ((inf X) ((sup Y) Z)))) % 0.61/0.79 FOF formula (forall (X:a) (Y:a), (((eq Prop) (((modula1727524044comp_a less_eq) X) Y)) ((and (((less_eq X) Y)->False)) (((less_eq Y) X)->False)))) of role axiom named fact_129_local_Oincomp__def % 0.61/0.79 A new axiom: (forall (X:a) (Y:a), (((eq Prop) (((modula1727524044comp_a less_eq) X) Y)) ((and (((less_eq X) Y)->False)) (((less_eq Y) X)->False)))) % 0.61/0.79 FOF formula (forall (A:a) (B:a) (C:a), (((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) C) A) B))) of role axiom named fact_130_local_Oc__a % 0.61/0.79 A new axiom: (forall (A:a) (B:a) (C:a), (((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) C) A) B))) % 0.61/0.79 FOF formula (forall (A:a), ((less_eq A) A)) of role axiom named fact_131_local_Oorder_Orefl % 0.61/0.79 A new axiom: (forall (A:a), ((less_eq A) A)) % 0.61/0.79 FOF formula (forall (X:a), ((less_eq X) X)) of role axiom named fact_132_local_Oorder__refl % 0.61/0.79 A new axiom: (forall (X:a), ((less_eq X) X)) % 0.61/0.79 FOF formula (forall (P:(a->Prop)) (X:a) (Q:(a->Prop)), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq Y2) X)))->((forall (X2:a), ((P X2)->((forall (Y5:a), ((P Y5)->((less_eq Y5) X2)))->(Q X2))))->(Q ((greatest_a less_eq) P)))))) of role axiom named fact_133_local_OGreatestI2__order % 0.61/0.79 A new axiom: (forall (P:(a->Prop)) (X:a) (Q:(a->Prop)), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq Y2) X)))->((forall (X2:a), ((P X2)->((forall (Y5:a), ((P Y5)->((less_eq Y5) X2)))->(Q X2))))->(Q ((greatest_a less_eq) P)))))) % 0.61/0.79 FOF formula (forall (P:(a->Prop)) (X:a), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq Y2) X)))->(((eq a) ((greatest_a less_eq) P)) X)))) of role axiom named fact_134_local_OGreatest__equality % 0.61/0.79 A new axiom: (forall (P:(a->Prop)) (X:a), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq Y2) X)))->(((eq a) ((greatest_a less_eq) P)) X)))) % 0.61/0.79 FOF formula (forall (A:a) (B:a), ((and (((less_eq A) B)->(((eq a) (((max_a less_eq) A) B)) B))) ((((less_eq A) B)->False)->(((eq a) (((max_a less_eq) A) B)) A)))) of role axiom named fact_135_local_Omax__def % 0.61/0.79 A new axiom: (forall (A:a) (B:a), ((and (((less_eq A) B)->(((eq a) (((max_a less_eq) A) B)) B))) ((((less_eq A) B)->False)->(((eq a) (((max_a less_eq) A) B)) A)))) % 0.61/0.79 FOF formula (forall (A:a) (B:a), ((and (((less_eq A) B)->(((eq a) (((min_a less_eq) A) B)) A))) ((((less_eq A) B)->False)->(((eq a) (((min_a less_eq) A) B)) B)))) of role axiom named fact_136_local_Omin__def % 0.61/0.79 A new axiom: (forall (A:a) (B:a), ((and (((less_eq A) B)->(((eq a) (((min_a less_eq) A) B)) A))) ((((less_eq A) B)->False)->(((eq a) (((min_a less_eq) A) B)) B)))) % 0.61/0.79 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula17988509_aux_a inf) sup) A) B) C)) ((inf ((sup A) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))) of role axiom named fact_137_a__def__equiv % 0.61/0.79 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula17988509_aux_a inf) sup) A) B) C)) ((inf ((sup A) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))) % 0.61/0.79 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) ((inf ((sup C) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))) of role axiom named fact_138_c__def__equiv % 0.61/0.79 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) ((inf ((sup C) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))) % 0.61/0.81 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) ((inf ((sup B) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))) of role axiom named fact_139_b__def__equiv % 0.61/0.81 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) ((inf ((sup B) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))) % 0.61/0.81 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula581031071_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) of role axiom named fact_140_c__meet__a__eq__d % 0.61/0.81 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula581031071_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) % 0.61/0.81 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula17988509_aux_a inf) sup) A) B) C)) (((((modula1373251614_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) of role axiom named fact_141_a__meet__b__eq__d % 0.61/0.81 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula17988509_aux_a inf) sup) A) B) C)) (((((modula1373251614_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) % 0.61/0.81 FOF formula (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula1373251614_aux_a inf) sup) A) B) C)) (((((modula581031071_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) of role axiom named fact_142_b__meet__c__eq__d % 0.61/0.81 A new axiom: (forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula1373251614_aux_a inf) sup) A) B) C)) (((((modula581031071_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))) % 0.61/0.81 FOF formula (forall (X:a) (Y:a) (Z:a), (((eq Prop) ((less_eq X) ((inf Y) Z))) ((and ((less_eq X) Y)) ((less_eq X) Z)))) of role axiom named fact_143_local_Ole__inf__iff % 0.61/0.81 A new axiom: (forall (X:a) (Y:a) (Z:a), (((eq Prop) ((less_eq X) ((inf Y) Z))) ((and ((less_eq X) Y)) ((less_eq X) Z)))) % 0.61/0.81 FOF formula (forall (A:a) (B:a) (C:a), (((eq Prop) ((less_eq A) ((inf B) C))) ((and ((less_eq A) B)) ((less_eq A) C)))) of role axiom named fact_144_local_Oinf_Obounded__iff % 0.61/0.81 A new axiom: (forall (A:a) (B:a) (C:a), (((eq Prop) ((less_eq A) ((inf B) C))) ((and ((less_eq A) B)) ((less_eq A) C)))) % 0.61/0.81 FOF formula (forall (B:a) (C:a) (A:a), (((eq Prop) ((less_eq ((sup B) C)) A)) ((and ((less_eq B) A)) ((less_eq C) A)))) of role axiom named fact_145_local_Osup_Obounded__iff % 0.61/0.81 A new axiom: (forall (B:a) (C:a) (A:a), (((eq Prop) ((less_eq ((sup B) C)) A)) ((and ((less_eq B) A)) ((less_eq C) A)))) % 0.61/0.81 FOF formula (forall (X:a) (Y:a) (Z:a), (((eq Prop) ((less_eq ((sup X) Y)) Z)) ((and ((less_eq X) Z)) ((less_eq Y) Z)))) of role axiom named fact_146_local_Ole__sup__iff % 0.61/0.81 A new axiom: (forall (X:a) (Y:a) (Z:a), (((eq Prop) ((less_eq ((sup X) Y)) Z)) ((and ((less_eq X) Z)) ((less_eq Y) Z)))) % 0.61/0.81 FOF formula (forall (P:(a->Prop)), (((ex a) (fun (X4:a)=> ((and ((and (P X4)) (forall (Y2:a), ((P Y2)->((less_eq X4) Y2))))) (forall (Y2:a), (((and (P Y2)) (forall (Ya:a), ((P Ya)->((less_eq Y2) Ya))))->(((eq a) Y2) X4))))))->(P ((least_a less_eq) P)))) of role axiom named fact_147_local_OLeast1I % 0.61/0.82 A new axiom: (forall (P:(a->Prop)), (((ex a) (fun (X4:a)=> ((and ((and (P X4)) (forall (Y2:a), ((P Y2)->((less_eq X4) Y2))))) (forall (Y2:a), (((and (P Y2)) (forall (Ya:a), ((P Ya)->((less_eq Y2) Ya))))->(((eq a) Y2) X4))))))->(P ((least_a less_eq) P)))) % 0.61/0.82 FOF formula (forall (P:(a->Prop)) (Z:a), (((ex a) (fun (X4:a)=> ((and ((and (P X4)) (forall (Y2:a), ((P Y2)->((less_eq X4) Y2))))) (forall (Y2:a), (((and (P Y2)) (forall (Ya:a), ((P Ya)->((less_eq Y2) Ya))))->(((eq a) Y2) X4))))))->((P Z)->((less_eq ((least_a less_eq) P)) Z)))) of role axiom named fact_148_local_OLeast1__le % 0.61/0.82 A new axiom: (forall (P:(a->Prop)) (Z:a), (((ex a) (fun (X4:a)=> ((and ((and (P X4)) (forall (Y2:a), ((P Y2)->((less_eq X4) Y2))))) (forall (Y2:a), (((and (P Y2)) (forall (Ya:a), ((P Ya)->((less_eq Y2) Ya))))->(((eq a) Y2) X4))))))->((P Z)->((less_eq ((least_a less_eq) P)) Z)))) % 0.61/0.82 FOF formula (forall (P:(a->Prop)) (X:a) (Q:(a->Prop)), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq X) Y2)))->((forall (X2:a), ((P X2)->((forall (Y5:a), ((P Y5)->((less_eq X2) Y5)))->(Q X2))))->(Q ((least_a less_eq) P)))))) of role axiom named fact_149_local_OLeastI2__order % 0.61/0.82 A new axiom: (forall (P:(a->Prop)) (X:a) (Q:(a->Prop)), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq X) Y2)))->((forall (X2:a), ((P X2)->((forall (Y5:a), ((P Y5)->((less_eq X2) Y5)))->(Q X2))))->(Q ((least_a less_eq) P)))))) % 0.61/0.82 FOF formula (forall (P:(a->Prop)) (X:a), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq X) Y2)))->(((eq a) ((least_a less_eq) P)) X)))) of role axiom named fact_150_local_OLeast__equality % 0.61/0.82 A new axiom: (forall (P:(a->Prop)) (X:a), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq X) Y2)))->(((eq a) ((least_a less_eq) P)) X)))) % 0.61/0.82 FOF formula (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula581031071_aux_a) modula581031071_aux_a) of role axiom named fact_151_lattice_Oc__aux_Ocong % 0.61/0.82 A new axiom: (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula581031071_aux_a) modula581031071_aux_a) % 0.61/0.82 FOF formula (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1373251614_aux_a) modula1373251614_aux_a) of role axiom named fact_152_lattice_Ob__aux_Ocong % 0.61/0.82 A new axiom: (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1373251614_aux_a) modula1373251614_aux_a) % 0.61/0.82 FOF formula (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula17988509_aux_a) modula17988509_aux_a) of role axiom named fact_153_lattice_Oa__aux_Ocong % 0.61/0.82 A new axiom: (((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula17988509_aux_a) modula17988509_aux_a) % 0.61/0.82 FOF formula (forall (F:(a->(a->a))), ((abel_semigroup_a F)->(semigroup_a F))) of role axiom named fact_154_abel__semigroup_Oaxioms_I1_J % 0.61/0.82 A new axiom: (forall (F:(a->(a->a))), ((abel_semigroup_a F)->(semigroup_a F))) % 0.61/0.82 FOF formula (((eq ((a->(a->a))->Prop)) lattic1885654924_set_a) semilattice_a) of role axiom named fact_155_semilattice__set__def % 0.61/0.82 A new axiom: (((eq ((a->(a->a))->Prop)) lattic1885654924_set_a) semilattice_a) % 0.61/0.82 FOF formula (forall (F:(a->(a->a))), ((semilattice_a F)->(lattic1885654924_set_a F))) of role axiom named fact_156_semilattice__set_Ointro % 0.61/0.82 A new axiom: (forall (F:(a->(a->a))), ((semilattice_a F)->(lattic1885654924_set_a F))) % 0.61/0.82 FOF formula (forall (F:(a->(a->a))), ((lattic1885654924_set_a F)->(semilattice_a F))) of role axiom named fact_157_semilattice__set_Oaxioms % 0.61/0.82 A new axiom: (forall (F:(a->(a->a))), ((lattic1885654924_set_a F)->(semilattice_a F))) % 0.61/0.82 FOF formula (forall (F:(a->(a->a))), ((semilattice_a F)->(abel_semigroup_a F))) of role axiom named fact_158_semilattice_Oaxioms_I1_J % 0.61/0.82 A new axiom: (forall (F:(a->(a->a))), ((semilattice_a F)->(abel_semigroup_a F))) % 0.61/0.82 FOF formula (forall (A2:set_a), (((eq Prop) ((condit1627435690bove_a less_eq) A2)) ((ex a) (fun (M:a)=> (forall (X3:a), (((member_a X3) A2)->((less_eq X3) M))))))) of role axiom named fact_159_local_Obdd__above__def % 0.61/0.82 A new axiom: (forall (A2:set_a), (((eq Prop) ((condit1627435690bove_a less_eq) A2)) ((ex a) (fun (M:a)=> (forall (X3:a), (((member_a X3) A2)->((less_eq X3) M))))))) % 0.61/0.84 FOF formula (forall (A2:set_a), (((eq Prop) ((condit1001553558elow_a less_eq) A2)) ((ex a) (fun (M2:a)=> (forall (X3:a), (((member_a X3) A2)->((less_eq M2) X3))))))) of role axiom named fact_160_local_Obdd__below__def % 0.61/0.84 A new axiom: (forall (A2:set_a), (((eq Prop) ((condit1001553558elow_a less_eq) A2)) ((ex a) (fun (M2:a)=> (forall (X3:a), (((member_a X3) A2)->((less_eq M2) X3))))))) % 0.61/0.84 FOF formula (forall (A2:set_a) (M3:a), ((forall (X2:a), (((member_a X2) A2)->((less_eq M3) X2)))->((condit1001553558elow_a less_eq) A2))) of role axiom named fact_161_local_Obdd__belowI % 0.61/0.84 A new axiom: (forall (A2:set_a) (M3:a), ((forall (X2:a), (((member_a X2) A2)->((less_eq M3) X2)))->((condit1001553558elow_a less_eq) A2))) % 0.61/0.84 FOF formula (forall (A2:set_a) (M4:a), ((forall (X2:a), (((member_a X2) A2)->((less_eq X2) M4)))->((condit1627435690bove_a less_eq) A2))) of role axiom named fact_162_local_Obdd__aboveI % 0.61/0.84 A new axiom: (forall (A2:set_a) (M4:a), ((forall (X2:a), (((member_a X2) A2)->((less_eq X2) M4)))->((condit1627435690bove_a less_eq) A2))) % 0.61/0.84 FOF formula (((eq ((a->(a->Prop))->(a->(a->Prop)))) modula1727524044comp_a) modula1727524044comp_a) of role axiom named fact_163_lattice_Oincomp_Ocong % 0.61/0.84 A new axiom: (((eq ((a->(a->Prop))->(a->(a->Prop)))) modula1727524044comp_a) modula1727524044comp_a) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))) (B:a) (A:a) (C:a), ((abel_semigroup_a F)->(((eq a) ((F B) ((F A) C))) ((F A) ((F B) C))))) of role axiom named fact_164_abel__semigroup_Oleft__commute % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))) (B:a) (A:a) (C:a), ((abel_semigroup_a F)->(((eq a) ((F B) ((F A) C))) ((F A) ((F B) C))))) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a), ((semilattice_a F)->(((eq a) ((F ((F A) B)) B)) ((F A) B)))) of role axiom named fact_165_semilattice_Oright__idem % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a), ((semilattice_a F)->(((eq a) ((F ((F A) B)) B)) ((F A) B)))) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a), ((semilattice_a F)->(((eq a) ((F A) ((F A) B))) ((F A) B)))) of role axiom named fact_166_semilattice_Oleft__idem % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a), ((semilattice_a F)->(((eq a) ((F A) ((F A) B))) ((F A) B)))) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a), ((abel_semigroup_a F)->(((eq a) ((F A) B)) ((F B) A)))) of role axiom named fact_167_abel__semigroup_Ocommute % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a), ((abel_semigroup_a F)->(((eq a) ((F A) B)) ((F B) A)))) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))) (A:a), ((semilattice_a F)->(((eq a) ((F A) A)) A))) of role axiom named fact_168_semilattice_Oidem % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))) (A:a), ((semilattice_a F)->(((eq a) ((F A) A)) A))) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))), ((forall (A4:a) (B3:a) (C2:a), (((eq a) ((F ((F A4) B3)) C2)) ((F A4) ((F B3) C2))))->(semigroup_a F))) of role axiom named fact_169_semigroup_Ointro % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))), ((forall (A4:a) (B3:a) (C2:a), (((eq a) ((F ((F A4) B3)) C2)) ((F A4) ((F B3) C2))))->(semigroup_a F))) % 0.61/0.84 FOF formula (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((semigroup_a F)->(((eq a) ((F ((F A) B)) C)) ((F A) ((F B) C))))) of role axiom named fact_170_semigroup_Oassoc % 0.61/0.84 A new axiom: (forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((semigroup_a F)->(((eq a) ((F ((F A) B)) C)) ((F A) ((F B) C))))) % 0.61/0.84 FOF formula (((eq ((a->(a->a))->Prop)) semigroup_a) (fun (F2:(a->(a->a)))=> (forall (A3:a) (B2:a) (C3:a), (((eq a) ((F2 ((F2 A3) B2)) C3)) ((F2 A3) ((F2 B2) C3)))))) of role axiom named fact_171_semigroup__def % 0.61/0.84 A new axiom: (((eq ((a->(a->a))->Prop)) semigroup_a) (fun (F2:(a->(a->a)))=> (forall (A3:a) (B2:a) (C3:a), (((eq a) ((F2 ((F2 A3) B2)) C3)) ((F2 A3) ((F2 B2) C3)))))) % 0.61/0.84 FOF formula (forall (B4:set_a) (A2:set_a), (((condit1001553558elow_a less_eq) B4)->(((ord_less_eq_set_a A2) B4)->((condit1001553558elow_a less_eq) A2)))) of role axiom named fact_172_local_Obdd__below__mono % 0.61/0.84 A new axiom: (forall (B4:set_a) (A2:set_a), (((condit1001553558elow_a less_eq) B4)->(((ord_less_eq_set_a A2) B4)->((condit1001553558elow_a less_eq) A2)))) % 0.61/0.85 FOF formula (forall (B4:set_a) (A2:set_a), (((condit1627435690bove_a less_eq) B4)->(((ord_less_eq_set_a A2) B4)->((condit1627435690bove_a less_eq) A2)))) of role axiom named fact_173_local_Obdd__above__mono % 0.61/0.85 A new axiom: (forall (B4:set_a) (A2:set_a), (((condit1627435690bove_a less_eq) B4)->(((ord_less_eq_set_a A2) B4)->((condit1627435690bove_a less_eq) A2)))) % 0.61/0.85 FOF formula (forall (A2:set_a), ((finite_finite_a A2)->((condit1001553558elow_a less_eq) A2))) of role axiom named fact_174_local_Obdd__below__finite % 0.61/0.85 A new axiom: (forall (A2:set_a), ((finite_finite_a A2)->((condit1001553558elow_a less_eq) A2))) % 0.61/0.85 FOF formula (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((ex a) (fun (X2:a)=> ((and ((and ((member_a X2) A2)) ((less_eq A) X2))) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq X2) Xa)->(((eq a) X2) Xa)))))))))) of role axiom named fact_175_local_Ofinite__has__maximal2 % 0.61/0.85 A new axiom: (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((ex a) (fun (X2:a)=> ((and ((and ((member_a X2) A2)) ((less_eq A) X2))) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq X2) Xa)->(((eq a) X2) Xa)))))))))) % 0.61/0.85 FOF formula (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((ex a) (fun (X2:a)=> ((and ((and ((member_a X2) A2)) ((less_eq X2) A))) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq Xa) X2)->(((eq a) X2) Xa)))))))))) of role axiom named fact_176_local_Ofinite__has__minimal2 % 0.61/0.85 A new axiom: (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((ex a) (fun (X2:a)=> ((and ((and ((member_a X2) A2)) ((less_eq X2) A))) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq Xa) X2)->(((eq a) X2) Xa)))))))))) % 0.61/0.85 FOF formula (forall (A2:set_a), ((finite_finite_a A2)->((condit1627435690bove_a less_eq) A2))) of role axiom named fact_177_local_Obdd__above__finite % 0.61/0.85 A new axiom: (forall (A2:set_a), ((finite_finite_a A2)->((condit1627435690bove_a less_eq) A2))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)) (X:a) (Y:a), (((antimono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F Y)) (F X))))) of role axiom named fact_178_local_OantimonoD % 0.61/0.85 A new axiom: (forall (F:(a->set_a)) (X:a) (Y:a), (((antimono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F Y)) (F X))))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)) (X:a) (Y:a), (((antimono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F Y)) (F X))))) of role axiom named fact_179_local_OantimonoE % 0.61/0.85 A new axiom: (forall (F:(a->set_a)) (X:a) (Y:a), (((antimono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F Y)) (F X))))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)), ((forall (X2:a) (Y2:a), (((less_eq X2) Y2)->((ord_less_eq_set_a (F Y2)) (F X2))))->((antimono_a_set_a less_eq) F))) of role axiom named fact_180_local_OantimonoI % 0.61/0.85 A new axiom: (forall (F:(a->set_a)), ((forall (X2:a) (Y2:a), (((less_eq X2) Y2)->((ord_less_eq_set_a (F Y2)) (F X2))))->((antimono_a_set_a less_eq) F))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)), (((eq Prop) ((antimono_a_set_a less_eq) F)) (forall (X3:a) (Y4:a), (((less_eq X3) Y4)->((ord_less_eq_set_a (F Y4)) (F X3)))))) of role axiom named fact_181_local_Oantimono__def % 0.61/0.85 A new axiom: (forall (F:(a->set_a)), (((eq Prop) ((antimono_a_set_a less_eq) F)) (forall (X3:a) (Y4:a), (((less_eq X3) Y4)->((ord_less_eq_set_a (F Y4)) (F X3)))))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)), (((eq Prop) ((mono_a_set_a less_eq) F)) (forall (X3:a) (Y4:a), (((less_eq X3) Y4)->((ord_less_eq_set_a (F X3)) (F Y4)))))) of role axiom named fact_182_local_Omono__def % 0.61/0.85 A new axiom: (forall (F:(a->set_a)), (((eq Prop) ((mono_a_set_a less_eq) F)) (forall (X3:a) (Y4:a), (((less_eq X3) Y4)->((ord_less_eq_set_a (F X3)) (F Y4)))))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)), ((forall (X2:a) (Y2:a), (((less_eq X2) Y2)->((ord_less_eq_set_a (F X2)) (F Y2))))->((mono_a_set_a less_eq) F))) of role axiom named fact_183_local_OmonoI % 0.61/0.85 A new axiom: (forall (F:(a->set_a)), ((forall (X2:a) (Y2:a), (((less_eq X2) Y2)->((ord_less_eq_set_a (F X2)) (F Y2))))->((mono_a_set_a less_eq) F))) % 0.61/0.85 FOF formula (forall (F:(a->set_a)) (X:a) (Y:a), (((mono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F X)) (F Y))))) of role axiom named fact_184_local_OmonoE % 0.61/0.86 A new axiom: (forall (F:(a->set_a)) (X:a) (Y:a), (((mono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F X)) (F Y))))) % 0.61/0.86 FOF formula (forall (F:(a->set_a)) (X:a) (Y:a), (((mono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F X)) (F Y))))) of role axiom named fact_185_local_OmonoD % 0.61/0.86 A new axiom: (forall (F:(a->set_a)) (X:a) (Y:a), (((mono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F X)) (F Y))))) % 0.61/0.86 FOF formula (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((less_eq A) ((lattic1781219155_fin_a sup) A2))))) of role axiom named fact_186_local_OSup__fin_OcoboundedI % 0.61/0.86 A new axiom: (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((less_eq A) ((lattic1781219155_fin_a sup) A2))))) % 0.61/0.86 FOF formula (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((less_eq ((lattic247676691_fin_a inf) A2)) A)))) of role axiom named fact_187_local_OInf__fin_OcoboundedI % 0.61/0.86 A new axiom: (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((less_eq ((lattic247676691_fin_a inf) A2)) A)))) % 0.61/0.86 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->(((member_a X) A2)->(((eq a) ((sup X) ((lattic1781219155_fin_a sup) A2))) ((lattic1781219155_fin_a sup) A2))))) of role axiom named fact_188_local_OSup__fin_Oin__idem % 0.61/0.86 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->(((member_a X) A2)->(((eq a) ((sup X) ((lattic1781219155_fin_a sup) A2))) ((lattic1781219155_fin_a sup) A2))))) % 0.61/0.86 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->(((member_a X) A2)->(((eq a) ((inf X) ((lattic247676691_fin_a inf) A2))) ((lattic247676691_fin_a inf) A2))))) of role axiom named fact_189_local_OInf__fin_Oin__idem % 0.61/0.86 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->(((member_a X) A2)->(((eq a) ((inf X) ((lattic247676691_fin_a inf) A2))) ((lattic247676691_fin_a inf) A2))))) % 0.61/0.86 FOF formula (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->(((eq a) ((sup ((lattic247676691_fin_a inf) A2)) A)) A)))) of role axiom named fact_190_local_Osup__Inf__absorb % 0.61/0.86 A new axiom: (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->(((eq a) ((sup ((lattic247676691_fin_a inf) A2)) A)) A)))) % 0.61/0.86 FOF formula (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->(((eq a) ((inf A) ((lattic1781219155_fin_a sup) A2))) A)))) of role axiom named fact_191_local_Oinf__Sup__absorb % 0.61/0.86 A new axiom: (forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->(((eq a) ((inf A) ((lattic1781219155_fin_a sup) A2))) A)))) % 0.61/0.86 FOF formula (((eq ((a->(a->a))->(set_a->a))) lattic247676691_fin_a) lattic247676691_fin_a) of role axiom named fact_192_semilattice__inf_OInf__fin_Ocong % 0.61/0.86 A new axiom: (((eq ((a->(a->a))->(set_a->a))) lattic247676691_fin_a) lattic247676691_fin_a) % 0.61/0.86 FOF formula (((eq ((a->(a->a))->(set_a->a))) lattic1781219155_fin_a) lattic1781219155_fin_a) of role axiom named fact_193_semilattice__sup_OSup__fin_Ocong % 0.61/0.86 A new axiom: (((eq ((a->(a->a))->(set_a->a))) lattic1781219155_fin_a) lattic1781219155_fin_a) % 0.61/0.86 FOF formula (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((less_eq ((lattic247676691_fin_a inf) A2)) ((lattic1781219155_fin_a sup) A2))))) of role axiom named fact_194_local_OInf__fin__le__Sup__fin % 0.61/0.86 A new axiom: (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((less_eq ((lattic247676691_fin_a inf) A2)) ((lattic1781219155_fin_a sup) A2))))) % 0.61/0.86 FOF formula (forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->((not (((eq set_a) A2) bot_bot_set_a))->((finite_finite_a B4)->((less_eq ((lattic1781219155_fin_a sup) A2)) ((lattic1781219155_fin_a sup) B4)))))) of role axiom named fact_195_local_OSup__fin_Osubset__imp % 0.61/0.86 A new axiom: (forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->((not (((eq set_a) A2) bot_bot_set_a))->((finite_finite_a B4)->((less_eq ((lattic1781219155_fin_a sup) A2)) ((lattic1781219155_fin_a sup) B4)))))) % 0.61/0.86 FOF formula (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((ex a) (fun (X2:a)=> ((and ((member_a X2) A2)) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq Xa) X2)->(((eq a) X2) Xa)))))))))) of role axiom named fact_196_local_Ofinite__has__minimal % 0.71/0.87 A new axiom: (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((ex a) (fun (X2:a)=> ((and ((member_a X2) A2)) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq Xa) X2)->(((eq a) X2) Xa)))))))))) % 0.71/0.87 FOF formula (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((ex a) (fun (X2:a)=> ((and ((member_a X2) A2)) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq X2) Xa)->(((eq a) X2) Xa)))))))))) of role axiom named fact_197_local_Ofinite__has__maximal % 0.71/0.87 A new axiom: (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((ex a) (fun (X2:a)=> ((and ((member_a X2) A2)) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq X2) Xa)->(((eq a) X2) Xa)))))))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (B4:set_a), ((finite_finite_a A2)->((not (((eq set_a) B4) bot_bot_set_a))->(((ord_less_eq_set_a B4) A2)->(((eq a) ((inf ((lattic247676691_fin_a inf) B4)) ((lattic247676691_fin_a inf) A2))) ((lattic247676691_fin_a inf) A2)))))) of role axiom named fact_198_local_OInf__fin_Osubset % 0.71/0.87 A new axiom: (forall (A2:set_a) (B4:set_a), ((finite_finite_a A2)->((not (((eq set_a) B4) bot_bot_set_a))->(((ord_less_eq_set_a B4) A2)->(((eq a) ((inf ((lattic247676691_fin_a inf) B4)) ((lattic247676691_fin_a inf) A2))) ((lattic247676691_fin_a inf) A2)))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (B4:set_a), ((finite_finite_a A2)->((not (((eq set_a) B4) bot_bot_set_a))->(((ord_less_eq_set_a B4) A2)->(((eq a) ((sup ((lattic1781219155_fin_a sup) B4)) ((lattic1781219155_fin_a sup) A2))) ((lattic1781219155_fin_a sup) A2)))))) of role axiom named fact_199_local_OSup__fin_Osubset % 0.71/0.87 A new axiom: (forall (A2:set_a) (B4:set_a), ((finite_finite_a A2)->((not (((eq set_a) B4) bot_bot_set_a))->(((ord_less_eq_set_a B4) A2)->(((eq a) ((sup ((lattic1781219155_fin_a sup) B4)) ((lattic1781219155_fin_a sup) A2))) ((lattic1781219155_fin_a sup) A2)))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq Prop) ((less_eq X) ((lattic247676691_fin_a inf) A2))) (forall (X3:a), (((member_a X3) A2)->((less_eq X) X3))))))) of role axiom named fact_200_local_OInf__fin_Obounded__iff % 0.71/0.87 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq Prop) ((less_eq X) ((lattic247676691_fin_a inf) A2))) (forall (X3:a), (((member_a X3) A2)->((less_eq X) X3))))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (A4:a), (((member_a A4) A2)->((less_eq X) A4)))->((less_eq X) ((lattic247676691_fin_a inf) A2)))))) of role axiom named fact_201_local_OInf__fin_OboundedI % 0.71/0.87 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (A4:a), (((member_a A4) A2)->((less_eq X) A4)))->((less_eq X) ((lattic247676691_fin_a inf) A2)))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((less_eq X) ((lattic247676691_fin_a inf) A2))->(forall (A5:a), (((member_a A5) A2)->((less_eq X) A5))))))) of role axiom named fact_202_local_OInf__fin_OboundedE % 0.71/0.87 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((less_eq X) ((lattic247676691_fin_a inf) A2))->(forall (A5:a), (((member_a A5) A2)->((less_eq X) A5))))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq Prop) ((less_eq ((lattic1781219155_fin_a sup) A2)) X)) (forall (X3:a), (((member_a X3) A2)->((less_eq X3) X))))))) of role axiom named fact_203_local_OSup__fin_Obounded__iff % 0.71/0.87 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq Prop) ((less_eq ((lattic1781219155_fin_a sup) A2)) X)) (forall (X3:a), (((member_a X3) A2)->((less_eq X3) X))))))) % 0.71/0.87 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (A4:a), (((member_a A4) A2)->((less_eq A4) X)))->((less_eq ((lattic1781219155_fin_a sup) A2)) X))))) of role axiom named fact_204_local_OSup__fin_OboundedI % 0.71/0.88 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (A4:a), (((member_a A4) A2)->((less_eq A4) X)))->((less_eq ((lattic1781219155_fin_a sup) A2)) X))))) % 0.71/0.88 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((less_eq ((lattic1781219155_fin_a sup) A2)) X)->(forall (A5:a), (((member_a A5) A2)->((less_eq A5) X))))))) of role axiom named fact_205_local_OSup__fin_OboundedE % 0.71/0.88 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((less_eq ((lattic1781219155_fin_a sup) A2)) X)->(forall (A5:a), (((member_a A5) A2)->((less_eq A5) X))))))) % 0.71/0.88 FOF formula (forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->((not (((eq set_a) A2) bot_bot_set_a))->((finite_finite_a B4)->((less_eq ((lattic247676691_fin_a inf) B4)) ((lattic247676691_fin_a inf) A2)))))) of role axiom named fact_206_local_OInf__fin_Osubset__imp % 0.71/0.88 A new axiom: (forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->((not (((eq set_a) A2) bot_bot_set_a))->((finite_finite_a B4)->((less_eq ((lattic247676691_fin_a inf) B4)) ((lattic247676691_fin_a inf) A2)))))) % 0.71/0.88 FOF formula ((condit1627435690bove_a less_eq) bot_bot_set_a) of role axiom named fact_207_local_Obdd__above__empty % 0.71/0.88 A new axiom: ((condit1627435690bove_a less_eq) bot_bot_set_a) % 0.71/0.88 FOF formula ((condit1001553558elow_a less_eq) bot_bot_set_a) of role axiom named fact_208_local_Obdd__below__empty % 0.71/0.88 A new axiom: ((condit1001553558elow_a less_eq) bot_bot_set_a) % 0.71/0.88 FOF formula (forall (H:a), (not (((eq set_a) bot_bot_set_a) ((set_atMost_a less_eq) H)))) of role axiom named fact_209_local_Onot__empty__eq__Iic__eq__empty % 0.71/0.88 A new axiom: (forall (H:a), (not (((eq set_a) bot_bot_set_a) ((set_atMost_a less_eq) H)))) % 0.71/0.88 FOF formula (forall (L:a), (not (((eq set_a) bot_bot_set_a) ((set_atLeast_a less_eq) L)))) of role axiom named fact_210_local_Onot__empty__eq__Ici__eq__empty % 0.71/0.88 A new axiom: (forall (L:a), (not (((eq set_a) bot_bot_set_a) ((set_atLeast_a less_eq) L)))) % 0.71/0.88 FOF formula (forall (_TPTP_I:a) (K:a), (((eq Prop) ((member_a _TPTP_I) ((set_atLeast_a less_eq) K))) ((less_eq K) _TPTP_I))) of role axiom named fact_211_local_OatLeast__iff % 0.71/0.88 A new axiom: (forall (_TPTP_I:a) (K:a), (((eq Prop) ((member_a _TPTP_I) ((set_atLeast_a less_eq) K))) ((less_eq K) _TPTP_I))) % 0.71/0.88 FOF formula (forall (_TPTP_I:a) (K:a), (((eq Prop) ((member_a _TPTP_I) ((set_atMost_a less_eq) K))) ((less_eq _TPTP_I) K))) of role axiom named fact_212_local_OatMost__iff % 0.71/0.88 A new axiom: (forall (_TPTP_I:a) (K:a), (((eq Prop) ((member_a _TPTP_I) ((set_atMost_a less_eq) K))) ((less_eq _TPTP_I) K))) % 0.71/0.88 FOF formula (forall (A:a), ((condit1001553558elow_a less_eq) ((set_atLeast_a less_eq) A))) of role axiom named fact_213_local_Obdd__below__Ici % 0.71/0.88 A new axiom: (forall (A:a), ((condit1001553558elow_a less_eq) ((set_atLeast_a less_eq) A))) % 0.71/0.88 FOF formula (forall (B:a), ((condit1627435690bove_a less_eq) ((set_atMost_a less_eq) B))) of role axiom named fact_214_local_Obdd__above__Iic % 0.71/0.88 A new axiom: (forall (B:a), ((condit1627435690bove_a less_eq) ((set_atMost_a less_eq) B))) % 0.71/0.88 FOF formula (forall (A2:set_a), ((ord_less_eq_set_a bot_bot_set_a) A2)) of role axiom named fact_215_empty__subsetI % 0.71/0.88 A new axiom: (forall (A2:set_a), ((ord_less_eq_set_a bot_bot_set_a) A2)) % 0.71/0.88 FOF formula (forall (A2:set_a), (((eq Prop) ((ord_less_eq_set_a A2) bot_bot_set_a)) (((eq set_a) A2) bot_bot_set_a))) of role axiom named fact_216_subset__empty % 0.71/0.88 A new axiom: (forall (A2:set_a), (((eq Prop) ((ord_less_eq_set_a A2) bot_bot_set_a)) (((eq set_a) A2) bot_bot_set_a))) % 0.71/0.88 FOF formula (forall (C:a), (((member_a C) bot_bot_set_a)->False)) of role axiom named fact_217_empty__iff % 0.71/0.88 A new axiom: (forall (C:a), (((member_a C) bot_bot_set_a)->False)) % 0.71/0.88 FOF formula (forall (A2:set_a), (((eq Prop) (forall (X3:a), (((member_a X3) A2)->False))) (((eq set_a) A2) bot_bot_set_a))) of role axiom named fact_218_all__not__in__conv % 0.73/0.89 A new axiom: (forall (A2:set_a), (((eq Prop) (forall (X3:a), (((member_a X3) A2)->False))) (((eq set_a) A2) bot_bot_set_a))) % 0.73/0.89 FOF formula (forall (P:(a->Prop)), (((eq Prop) (((eq set_a) (collect_a P)) bot_bot_set_a)) (forall (X3:a), ((P X3)->False)))) of role axiom named fact_219_Collect__empty__eq % 0.73/0.89 A new axiom: (forall (P:(a->Prop)), (((eq Prop) (((eq set_a) (collect_a P)) bot_bot_set_a)) (forall (X3:a), ((P X3)->False)))) % 0.73/0.89 FOF formula (forall (P:(a->Prop)), (((eq Prop) (((eq set_a) bot_bot_set_a) (collect_a P))) (forall (X3:a), ((P X3)->False)))) of role axiom named fact_220_empty__Collect__eq % 0.73/0.89 A new axiom: (forall (P:(a->Prop)), (((eq Prop) (((eq set_a) bot_bot_set_a) (collect_a P))) (forall (X3:a), ((P X3)->False)))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a), ((forall (X2:a), (((member_a X2) A2)->((member_a X2) B4)))->((ord_less_eq_set_a A2) B4))) of role axiom named fact_221_subsetI % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a), ((forall (X2:a), (((member_a X2) A2)->((member_a X2) B4)))->((ord_less_eq_set_a A2) B4))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) A2)->(((eq set_a) A2) B4)))) of role axiom named fact_222_subset__antisym % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) A2)->(((eq set_a) A2) B4)))) % 0.73/0.89 FOF formula (forall (A:a), (((member_a A) bot_bot_set_a)->False)) of role axiom named fact_223_emptyE % 0.73/0.89 A new axiom: (forall (A:a), (((member_a A) bot_bot_set_a)->False)) % 0.73/0.89 FOF formula (forall (A2:set_a) (A:a), ((((eq set_a) A2) bot_bot_set_a)->(((member_a A) A2)->False))) of role axiom named fact_224_equals0D % 0.73/0.89 A new axiom: (forall (A2:set_a) (A:a), ((((eq set_a) A2) bot_bot_set_a)->(((member_a A) A2)->False))) % 0.73/0.89 FOF formula (forall (A2:set_a), ((forall (Y2:a), (((member_a Y2) A2)->False))->(((eq set_a) A2) bot_bot_set_a))) of role axiom named fact_225_equals0I % 0.73/0.89 A new axiom: (forall (A2:set_a), ((forall (Y2:a), (((member_a Y2) A2)->False))->(((eq set_a) A2) bot_bot_set_a))) % 0.73/0.89 FOF formula (forall (A2:set_a), (((eq Prop) ((ex a) (fun (X3:a)=> ((member_a X3) A2)))) (not (((eq set_a) A2) bot_bot_set_a)))) of role axiom named fact_226_ex__in__conv % 0.73/0.89 A new axiom: (forall (A2:set_a), (((eq Prop) ((ex a) (fun (X3:a)=> ((member_a X3) A2)))) (not (((eq set_a) A2) bot_bot_set_a)))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a) (X:a), (((ord_less_eq_set_a A2) B4)->(((member_a X) A2)->((member_a X) B4)))) of role axiom named fact_227_in__mono % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a) (X:a), (((ord_less_eq_set_a A2) B4)->(((member_a X) A2)->((member_a X) B4)))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a) (C:a), (((ord_less_eq_set_a A2) B4)->(((member_a C) A2)->((member_a C) B4)))) of role axiom named fact_228_subsetD % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a) (C:a), (((ord_less_eq_set_a A2) B4)->(((member_a C) A2)->((member_a C) B4)))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) A2)->False))->False))) of role axiom named fact_229_equalityE % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) A2)->False))->False))) % 0.73/0.89 FOF formula (((eq (set_a->(set_a->Prop))) ord_less_eq_set_a) (fun (A6:set_a) (B5:set_a)=> (forall (X3:a), (((member_a X3) A6)->((member_a X3) B5))))) of role axiom named fact_230_subset__eq % 0.73/0.89 A new axiom: (((eq (set_a->(set_a->Prop))) ord_less_eq_set_a) (fun (A6:set_a) (B5:set_a)=> (forall (X3:a), (((member_a X3) A6)->((member_a X3) B5))))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((ord_less_eq_set_a A2) B4))) of role axiom named fact_231_equalityD1 % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((ord_less_eq_set_a A2) B4))) % 0.73/0.89 FOF formula (forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((ord_less_eq_set_a B4) A2))) of role axiom named fact_232_equalityD2 % 0.73/0.89 A new axiom: (forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((ord_less_eq_set_a B4) A2))) % 0.73/0.89 FOF formula (((eq (set_a->(set_a->Prop))) ord_less_eq_set_a) (fun (A6:set_a) (B5:set_a)=> (forall (T:a), (((member_a T) A6)->((member_a T) B5))))) of role axiom named fact_233_subset__iff % 0.73/0.90 A new axiom: (((eq (set_a->(set_a->Prop))) ord_less_eq_set_a) (fun (A6:set_a) (B5:set_a)=> (forall (T:a), (((member_a T) A6)->((member_a T) B5))))) % 0.73/0.90 FOF formula (forall (A2:set_a), ((ord_less_eq_set_a A2) A2)) of role axiom named fact_234_subset__refl % 0.73/0.90 A new axiom: (forall (A2:set_a), ((ord_less_eq_set_a A2) A2)) % 0.73/0.90 FOF formula (forall (P:(a->Prop)) (Q:(a->Prop)), ((forall (X2:a), ((P X2)->(Q X2)))->((ord_less_eq_set_a (collect_a P)) (collect_a Q)))) of role axiom named fact_235_Collect__mono % 0.73/0.90 A new axiom: (forall (P:(a->Prop)) (Q:(a->Prop)), ((forall (X2:a), ((P X2)->(Q X2)))->((ord_less_eq_set_a (collect_a P)) (collect_a Q)))) % 0.73/0.90 FOF formula (forall (A2:set_a) (B4:set_a) (C4:set_a), (((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) C4)->((ord_less_eq_set_a A2) C4)))) of role axiom named fact_236_subset__trans % 0.73/0.90 A new axiom: (forall (A2:set_a) (B4:set_a) (C4:set_a), (((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) C4)->((ord_less_eq_set_a A2) C4)))) % 0.73/0.90 FOF formula (((eq (set_a->(set_a->Prop))) (fun (Y3:set_a) (Z3:set_a)=> (((eq set_a) Y3) Z3))) (fun (A6:set_a) (B5:set_a)=> ((and ((ord_less_eq_set_a A6) B5)) ((ord_less_eq_set_a B5) A6)))) of role axiom named fact_237_set__eq__subset % 0.73/0.90 A new axiom: (((eq (set_a->(set_a->Prop))) (fun (Y3:set_a) (Z3:set_a)=> (((eq set_a) Y3) Z3))) (fun (A6:set_a) (B5:set_a)=> ((and ((ord_less_eq_set_a A6) B5)) ((ord_less_eq_set_a B5) A6)))) % 0.73/0.90 FOF formula (forall (P:(a->Prop)) (Q:(a->Prop)), (((eq Prop) ((ord_less_eq_set_a (collect_a P)) (collect_a Q))) (forall (X3:a), ((P X3)->(Q X3))))) of role axiom named fact_238_Collect__mono__iff % 0.73/0.90 A new axiom: (forall (P:(a->Prop)) (Q:(a->Prop)), (((eq Prop) ((ord_less_eq_set_a (collect_a P)) (collect_a Q))) (forall (X3:a), ((P X3)->(Q X3))))) % 0.73/0.90 FOF formula (forall (F:(a->set_a)) (A2:a) (B4:a), (((mono_a_set_a less_eq) F)->((ord_less_eq_set_a (F ((inf A2) B4))) ((inf_inf_set_a (F A2)) (F B4))))) of role axiom named fact_239_local_Omono__inf % 0.73/0.90 A new axiom: (forall (F:(a->set_a)) (A2:a) (B4:a), (((mono_a_set_a less_eq) F)->((ord_less_eq_set_a (F ((inf A2) B4))) ((inf_inf_set_a (F A2)) (F B4))))) % 0.73/0.90 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((((member_a X) A2)->False)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq a) ((lattic1781219155_fin_a sup) ((insert_a X) A2))) ((sup X) ((lattic1781219155_fin_a sup) A2))))))) of role axiom named fact_240_local_OSup__fin_Oinsert__not__elem % 0.73/0.90 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((((member_a X) A2)->False)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq a) ((lattic1781219155_fin_a sup) ((insert_a X) A2))) ((sup X) ((lattic1781219155_fin_a sup) A2))))))) % 0.73/0.90 FOF formula (forall (B4:set_a) (A2:set_a), (((condit1001553558elow_a less_eq) B4)->((condit1001553558elow_a less_eq) ((inf_inf_set_a A2) B4)))) of role axiom named fact_241_local_Obdd__below__Int2 % 0.73/0.90 A new axiom: (forall (B4:set_a) (A2:set_a), (((condit1001553558elow_a less_eq) B4)->((condit1001553558elow_a less_eq) ((inf_inf_set_a A2) B4)))) % 0.73/0.90 FOF formula (forall (A2:set_a) (B4:set_a), (((condit1001553558elow_a less_eq) A2)->((condit1001553558elow_a less_eq) ((inf_inf_set_a A2) B4)))) of role axiom named fact_242_local_Obdd__below__Int1 % 0.73/0.90 A new axiom: (forall (A2:set_a) (B4:set_a), (((condit1001553558elow_a less_eq) A2)->((condit1001553558elow_a less_eq) ((inf_inf_set_a A2) B4)))) % 0.73/0.90 FOF formula (forall (B4:set_a) (A2:set_a), (((condit1627435690bove_a less_eq) B4)->((condit1627435690bove_a less_eq) ((inf_inf_set_a A2) B4)))) of role axiom named fact_243_local_Obdd__above__Int2 % 0.73/0.90 A new axiom: (forall (B4:set_a) (A2:set_a), (((condit1627435690bove_a less_eq) B4)->((condit1627435690bove_a less_eq) ((inf_inf_set_a A2) B4)))) % 0.73/0.90 FOF formula (forall (A2:set_a) (B4:set_a), (((condit1627435690bove_a less_eq) A2)->((condit1627435690bove_a less_eq) ((inf_inf_set_a A2) B4)))) of role axiom named fact_244_local_Obdd__above__Int1 % 0.73/0.90 A new axiom: (forall (A2:set_a) (B4:set_a), (((condit1627435690bove_a less_eq) A2)->((condit1627435690bove_a less_eq) ((inf_inf_set_a A2) B4)))) % 0.73/0.91 FOF formula (forall (C4:set_a) (A2:set_a) (B4:set_a), (((eq Prop) ((ord_less_eq_set_a C4) ((inf_inf_set_a A2) B4))) ((and ((ord_less_eq_set_a C4) A2)) ((ord_less_eq_set_a C4) B4)))) of role axiom named fact_245_Int__subset__iff % 0.73/0.91 A new axiom: (forall (C4:set_a) (A2:set_a) (B4:set_a), (((eq Prop) ((ord_less_eq_set_a C4) ((inf_inf_set_a A2) B4))) ((and ((ord_less_eq_set_a C4) A2)) ((ord_less_eq_set_a C4) B4)))) % 0.73/0.91 FOF formula (forall (A:set_a), (((eq set_a) ((inf_inf_set_a A) A)) A)) of role axiom named fact_246_semilattice__inf__class_Oinf_Oidem % 0.73/0.91 A new axiom: (forall (A:set_a), (((eq set_a) ((inf_inf_set_a A) A)) A)) % 0.73/0.91 FOF formula (forall (X:set_a), (((eq set_a) ((inf_inf_set_a X) X)) X)) of role axiom named fact_247_semilattice__inf__class_Oinf__idem % 0.73/0.91 A new axiom: (forall (X:set_a), (((eq set_a) ((inf_inf_set_a X) X)) X)) % 0.73/0.91 FOF formula (forall (A:set_a) (B:set_a), (((eq set_a) ((inf_inf_set_a A) ((inf_inf_set_a A) B))) ((inf_inf_set_a A) B))) of role axiom named fact_248_semilattice__inf__class_Oinf_Oleft__idem % 0.73/0.92 A new axiom: (forall (A:set_a) (B:set_a), (((eq set_a) ((inf_inf_set_a A) ((inf_inf_set_a A) B))) ((inf_inf_set_a A) B))) % 0.73/0.92 FOF formula (forall (X:set_a) (Y:set_a), (((eq set_a) ((inf_inf_set_a X) ((inf_inf_set_a X) Y))) ((inf_inf_set_a X) Y))) of role axiom named fact_249_semilattice__inf__class_Oinf__left__idem % 0.73/0.92 A new axiom: (forall (X:set_a) (Y:set_a), (((eq set_a) ((inf_inf_set_a X) ((inf_inf_set_a X) Y))) ((inf_inf_set_a X) Y))) % 0.73/0.92 FOF formula (forall (A:set_a) (B:set_a), (((eq set_a) ((inf_inf_set_a ((inf_inf_set_a A) B)) B)) ((inf_inf_set_a A) B))) of role axiom named fact_250_semilattice__inf__class_Oinf_Oright__idem % 0.73/0.92 A new axiom: (forall (A:set_a) (B:set_a), (((eq set_a) ((inf_inf_set_a ((inf_inf_set_a A) B)) B)) ((inf_inf_set_a A) B))) % 0.73/0.92 FOF formula (forall (X:set_a) (Y:set_a), (((eq set_a) ((inf_inf_set_a ((inf_inf_set_a X) Y)) Y)) ((inf_inf_set_a X) Y))) of role axiom named fact_251_semilattice__inf__class_Oinf__right__idem % 0.73/0.92 A new axiom: (forall (X:set_a) (Y:set_a), (((eq set_a) ((inf_inf_set_a ((inf_inf_set_a X) Y)) Y)) ((inf_inf_set_a X) Y))) % 0.73/0.92 FOF formula (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (X2:a) (Y2:a), ((member_a ((inf X2) Y2)) ((insert_a X2) ((insert_a Y2) bot_bot_set_a))))->((member_a ((lattic247676691_fin_a inf) A2)) A2))))) of role axiom named fact_252_local_OInf__fin_Oclosed % 0.73/0.92 A new axiom: (forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (X2:a) (Y2:a), ((member_a ((inf X2) Y2)) ((insert_a X2) ((insert_a Y2) bot_bot_set_a))))->((member_a ((lattic247676691_fin_a inf) A2)) A2))))) % 0.73/0.92 FOF formula (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((((member_a X) A2)->False)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq a) ((lattic247676691_fin_a inf) ((insert_a X) A2))) ((inf X) ((lattic247676691_fin_a inf) A2))))))) of role axiom named fact_253_local_OInf__fin_Oinsert__not__elem % 0.73/0.92 A new axiom: (forall (A2:set_a) (X:a), ((finite_finite_a A2)->((((member_a X) A2)->False)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq a) ((lattic247676691_fin_a inf) ((insert_a X) A2))) ((inf X) ((lattic247676691_fin_a inf) A2))))))) % 0.73/0.92 FOF formula (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) of role conjecture named conj_0 % 0.73/0.92 Conjecture to prove = (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))):Prop % 0.73/0.92 We need to prove ['(((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c)))))'] % 0.73/0.92 Parameter set_a:Type. % 0.73/0.92 Parameter a:Type. % 0.73/0.92 Parameter condit1627435690bove_a:((a->(a->Prop))->(set_a->Prop)). % 0.73/0.92 Parameter condit1001553558elow_a:((a->(a->Prop))->(set_a->Prop)). % 0.73/0.92 Parameter finite40241356em_a_a:((a->(a->a))->Prop). % 0.73/0.92 Parameter finite_finite_a:(set_a->Prop). % 0.73/0.92 Parameter abel_semigroup_a:((a->(a->a))->Prop). % 0.73/0.92 Parameter semigroup_a:((a->(a->a))->Prop). % 0.73/0.92 Parameter inf_inf_set_a:(set_a->(set_a->set_a)). % 0.73/0.92 Parameter semilattice_a:((a->(a->a))->Prop). % 0.73/0.92 Parameter lattic247676691_fin_a:((a->(a->a))->(set_a->a)). % 0.73/0.92 Parameter lattic1885654924_set_a:((a->(a->a))->Prop). % 0.73/0.92 Parameter lattic1781219155_fin_a:((a->(a->a))->(set_a->a)). % 0.73/0.92 Parameter modula17988509_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))). % 0.73/0.92 Parameter modula1373251614_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))). % 0.73/0.92 Parameter modula581031071_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))). % 0.73/0.92 Parameter modula1936294176_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))). % 0.73/0.92 Parameter modula1144073633_aux_a:((a->(a->a))->((a->(a->a))->(a->(a->(a->a))))). % 0.73/0.92 Parameter modula1727524044comp_a:((a->(a->Prop))->(a->(a->Prop))). % 0.73/0.92 Parameter bot_bot_set_a:set_a. % 0.73/0.92 Parameter least_a:((a->(a->Prop))->((a->Prop)->a)). % 0.73/0.92 Parameter max_a:((a->(a->Prop))->(a->(a->a))). % 0.73/0.92 Parameter min_a:((a->(a->Prop))->(a->(a->a))). % 0.73/0.92 Parameter ord_less_eq_set_a:(set_a->(set_a->Prop)). % 0.73/0.92 Parameter greatest_a:((a->(a->Prop))->((a->Prop)->a)). % 0.73/0.92 Parameter antimono_a_set_a:((a->(a->Prop))->((a->set_a)->Prop)). % 0.73/0.92 Parameter mono_a_set_a:((a->(a->Prop))->((a->set_a)->Prop)). % 0.73/0.92 Parameter collect_a:((a->Prop)->set_a). % 0.73/0.92 Parameter insert_a:(a->(set_a->set_a)). % 0.73/0.92 Parameter set_atLeast_a:((a->(a->Prop))->(a->set_a)). % 0.73/0.92 Parameter set_atMost_a:((a->(a->Prop))->(a->set_a)). % 0.73/0.92 Parameter member_a:(a->(set_a->Prop)). % 0.73/0.92 Parameter a2:a. % 0.73/0.92 Parameter b:a. % 0.73/0.92 Parameter c:a. % 0.73/0.92 Parameter inf:(a->(a->a)). % 0.73/0.92 Parameter less_eq:(a->(a->Prop)). % 0.73/0.92 Parameter sup:(a->(a->a)). % 0.73/0.92 Axiom fact_0_local_Oinf_Oassoc:(forall (A:a) (B:a) (C:a), (((eq a) ((inf ((inf A) B)) C)) ((inf A) ((inf B) C)))). % 0.73/0.92 Axiom fact_1_local_Oinf_Ocommute:(forall (A:a) (B:a), (((eq a) ((inf A) B)) ((inf B) A))). % 0.73/0.92 Axiom fact_2_local_Oinf_Oleft__commute:(forall (B:a) (A:a) (C:a), (((eq a) ((inf B) ((inf A) C))) ((inf A) ((inf B) C)))). % 0.73/0.92 Axiom fact_3_local_Oinf__assoc:(forall (X:a) (Y:a) (Z:a), (((eq a) ((inf ((inf X) Y)) Z)) ((inf X) ((inf Y) Z)))). % 0.73/0.92 Axiom fact_4_local_Oinf__commute:(forall (X:a) (Y:a), (((eq a) ((inf X) Y)) ((inf Y) X))). % 0.73/0.92 Axiom fact_5_local_Oinf__left__commute:(forall (X:a) (Y:a) (Z:a), (((eq a) ((inf X) ((inf Y) Z))) ((inf Y) ((inf X) Z)))). % 0.73/0.92 Axiom fact_6_local_Osup_Oassoc:(forall (A:a) (B:a) (C:a), (((eq a) ((sup ((sup A) B)) C)) ((sup A) ((sup B) C)))). % 0.73/0.92 Axiom fact_7_local_Osup_Ocommute:(forall (A:a) (B:a), (((eq a) ((sup A) B)) ((sup B) A))). % 0.73/0.92 Axiom fact_8_local_Osup_Oleft__commute:(forall (B:a) (A:a) (C:a), (((eq a) ((sup B) ((sup A) C))) ((sup A) ((sup B) C)))). % 0.73/0.92 Axiom fact_9_local_Osup__assoc:(forall (X:a) (Y:a) (Z:a), (((eq a) ((sup ((sup X) Y)) Z)) ((sup X) ((sup Y) Z)))). % 0.73/0.92 Axiom fact_10_local_Osup__commute:(forall (X:a) (Y:a), (((eq a) ((sup X) Y)) ((sup Y) X))). % 0.73/0.92 Axiom fact_11_local_Osup__left__commute:(forall (X:a) (Y:a) (Z:a), (((eq a) ((sup X) ((sup Y) Z))) ((sup Y) ((sup X) Z)))). % 0.73/0.92 Axiom fact_12_local_Odistrib__imp1:(forall (X:a) (Y:a) (Z:a), ((forall (X2:a) (Y2:a) (Z2:a), (((eq a) ((inf X2) ((sup Y2) Z2))) ((sup ((inf X2) Y2)) ((inf X2) Z2))))->(((eq a) ((sup X) ((inf Y) Z))) ((inf ((sup X) Y)) ((sup X) Z))))). % 0.73/0.92 Axiom fact_13_local_Odistrib__imp2:(forall (X:a) (Y:a) (Z:a), ((forall (X2:a) (Y2:a) (Z2:a), (((eq a) ((sup X2) ((inf Y2) Z2))) ((inf ((sup X2) Y2)) ((sup X2) Z2))))->(((eq a) ((inf X) ((sup Y) Z))) ((sup ((inf X) Y)) ((inf X) Z))))). % 0.73/0.92 Axiom fact_14_local_Oa__join__d:(forall (A:a) (B:a) (C:a), (((eq a) ((sup A) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup A) ((inf B) C)))). % 0.73/0.92 Axiom fact_15_a__meet__d:(forall (A:a) (B:a) (C:a), (((eq a) ((inf A) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf A) B)) ((inf C) A)))). % 0.73/0.92 Axiom fact_16_local_Ob__join__d:(forall (B:a) (A:a) (C:a), (((eq a) ((sup B) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup B) ((inf C) A)))). % 0.73/0.92 Axiom fact_17_b__meet__d:(forall (B:a) (A:a) (C:a), (((eq a) ((inf B) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf B) C)) ((inf A) B)))). % 0.73/0.92 Axiom fact_18_c__meet__d:(forall (C:a) (A:a) (B:a), (((eq a) ((inf C) (((((modula1936294176_aux_a inf) sup) A) B) C))) ((sup ((inf C) A)) ((inf B) C)))). % 0.73/0.92 Axiom fact_19_local_Od__aux__def:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula1936294176_aux_a inf) sup) A) B) C)) ((sup ((sup ((inf A) B)) ((inf B) C))) ((inf C) A)))). % 0.73/0.92 Axiom fact_20_local_Od__b__c__a:(forall (B:a) (C:a) (A:a), (((eq a) (((((modula1936294176_aux_a inf) sup) B) C) A)) (((((modula1936294176_aux_a inf) sup) A) B) C))). % 0.73/0.92 Axiom fact_21_local_Od__c__a__b:(forall (C:a) (A:a) (B:a), (((eq a) (((((modula1936294176_aux_a inf) sup) C) A) B)) (((((modula1936294176_aux_a inf) sup) A) B) C))). % 0.73/0.92 Axiom fact_22_local_Oa__meet__e:(forall (A:a) (B:a) (C:a), (((eq a) ((inf A) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf A) ((sup B) C)))). % 0.73/0.92 Axiom fact_23_local_Ob__meet__e:(forall (B:a) (A:a) (C:a), (((eq a) ((inf B) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf B) ((sup C) A)))). % 0.73/0.92 Axiom fact_24_local_Oc__meet__e:(forall (C:a) (A:a) (B:a), (((eq a) ((inf C) (((((modula1144073633_aux_a inf) sup) A) B) C))) ((inf C) ((sup A) B)))). % 0.73/0.92 Axiom fact_25_local_Oe__aux__def:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula1144073633_aux_a inf) sup) A) B) C)) ((inf ((inf ((sup A) B)) ((sup B) C))) ((sup C) A)))). % 0.73/0.92 Axiom fact_26_local_Oe__b__c__a:(forall (B:a) (C:a) (A:a), (((eq a) (((((modula1144073633_aux_a inf) sup) B) C) A)) (((((modula1144073633_aux_a inf) sup) A) B) C))). % 0.73/0.92 Axiom fact_27_local_Oe__c__a__b:(forall (C:a) (A:a) (B:a), (((eq a) (((((modula1144073633_aux_a inf) sup) C) A) B)) (((((modula1144073633_aux_a inf) sup) A) B) C))). % 0.73/0.92 Axiom fact_28_local_Oinf_Oidem:(forall (A:a), (((eq a) ((inf A) A)) A)). % 0.73/0.92 Axiom fact_29_local_Oinf_Oleft__idem:(forall (A:a) (B:a), (((eq a) ((inf A) ((inf A) B))) ((inf A) B))). % 0.73/0.92 Axiom fact_30_local_Oinf_Oright__idem:(forall (A:a) (B:a), (((eq a) ((inf ((inf A) B)) B)) ((inf A) B))). % 0.73/0.92 Axiom fact_31_local_Oinf__idem:(forall (X:a), (((eq a) ((inf X) X)) X)). % 0.73/0.92 Axiom fact_32_local_Oinf__left__idem:(forall (X:a) (Y:a), (((eq a) ((inf X) ((inf X) Y))) ((inf X) Y))). % 0.73/0.92 Axiom fact_33_local_Oinf__right__idem:(forall (X:a) (Y:a), (((eq a) ((inf ((inf X) Y)) Y)) ((inf X) Y))). % 0.73/0.92 Axiom fact_34_local_Osup_Oidem:(forall (A:a), (((eq a) ((sup A) A)) A)). % 0.73/0.92 Axiom fact_35_local_Osup_Oleft__idem:(forall (A:a) (B:a), (((eq a) ((sup A) ((sup A) B))) ((sup A) B))). % 0.73/0.92 Axiom fact_36_local_Osup_Oright__idem:(forall (A:a) (B:a), (((eq a) ((sup ((sup A) B)) B)) ((sup A) B))). % 0.73/0.92 Axiom fact_37_local_Osup__idem:(forall (X:a), (((eq a) ((sup X) X)) X)). % 0.73/0.92 Axiom fact_38_local_Osup__left__idem:(forall (X:a) (Y:a), (((eq a) ((sup X) ((sup X) Y))) ((sup X) Y))). % 0.73/0.92 Axiom fact_39_calculation:(((eq a) ((sup ((inf ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)))) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))). % 0.73/0.92 Axiom fact_40_local_Oinf__sup__absorb:(forall (X:a) (Y:a), (((eq a) ((inf X) ((sup X) Y))) X)). % 0.73/0.92 Axiom fact_41_local_Osup__inf__absorb:(forall (X:a) (Y:a), (((eq a) ((sup X) ((inf X) Y))) X)). % 0.77/0.92 Axiom fact_42_local_Ob__aux__def:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) ((sup ((inf B) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))). % 0.77/0.92 Axiom fact_43_local_Oc__aux__def:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) ((sup ((inf C) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))). % 0.77/0.92 Axiom fact_44_local_Oa__aux__def:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula17988509_aux_a inf) sup) A) B) C)) ((sup ((inf A) (((((modula1144073633_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))). % 0.77/0.92 Axiom fact_45_mem__Collect__eq:(forall (A:a) (P:(a->Prop)), (((eq Prop) ((member_a A) (collect_a P))) (P A))). % 0.77/0.92 Axiom fact_46_Collect__mem__eq:(forall (A2:set_a), (((eq set_a) (collect_a (fun (X3:a)=> ((member_a X3) A2)))) A2)). % 0.77/0.92 Axiom fact_47_Collect__cong:(forall (P:(a->Prop)) (Q:(a->Prop)), ((forall (X2:a), (((eq Prop) (P X2)) (Q X2)))->(((eq set_a) (collect_a P)) (collect_a Q)))). % 0.77/0.92 Axiom fact_48_lattice_Od__aux_Ocong:(((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1936294176_aux_a) modula1936294176_aux_a). % 0.77/0.92 Axiom fact_49_lattice_Oe__aux_Ocong:(((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1144073633_aux_a) modula1144073633_aux_a). % 0.77/0.92 Axiom fact_50_d__less__e:((less_eq (((((modula1936294176_aux_a inf) sup) a2) b) c)) (((((modula1144073633_aux_a inf) sup) a2) b) c)). % 0.77/0.92 Axiom fact_51_local_Ocomp__fun__idem__sup:(finite40241356em_a_a sup). % 0.77/0.92 Axiom fact_52_local_Ocomp__fun__idem__inf:(finite40241356em_a_a inf). % 0.77/0.92 Axiom fact_53_local_Osup_Osemigroup__axioms:(semigroup_a sup). % 0.77/0.92 Axiom fact_54_local_Oinf_Osemigroup__axioms:(semigroup_a inf). % 0.77/0.92 Axiom fact_55_local_Osup_Osemilattice__axioms:(semilattice_a sup). % 0.77/0.92 Axiom fact_56_local_Oinf_Osemilattice__axioms:(semilattice_a inf). % 0.77/0.92 Axiom fact_57_local_Osup_Oabel__semigroup__axioms:(abel_semigroup_a sup). % 0.77/0.92 Axiom fact_58_local_Oinf_Oabel__semigroup__axioms:(abel_semigroup_a inf). % 0.77/0.92 Axiom fact_59_local_OSup__fin_Osemilattice__set__axioms:(lattic1885654924_set_a sup). % 0.77/0.92 Axiom fact_60_local_OInf__fin_Osemilattice__set__axioms:(lattic1885654924_set_a inf). % 0.77/0.92 Axiom fact_61_local_Ob__a:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) B) C) A))). % 0.77/0.92 Axiom fact_62_local_Oantisym:(forall (X:a) (Y:a), (((less_eq X) Y)->(((less_eq Y) X)->(((eq a) X) Y)))). % 0.77/0.92 Axiom fact_63_local_Oantisym__conv:(forall (Y:a) (X:a), (((less_eq Y) X)->(((eq Prop) ((less_eq X) Y)) (((eq a) X) Y)))). % 0.77/0.92 Axiom fact_64_local_Odual__order_Oantisym:(forall (B:a) (A:a), (((less_eq B) A)->(((less_eq A) B)->(((eq a) A) B)))). % 0.77/0.92 Axiom fact_65_local_Odual__order_Oeq__iff:(((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (A3:a) (B2:a)=> ((and ((less_eq B2) A3)) ((less_eq A3) B2)))). % 0.77/0.92 Axiom fact_66_local_Odual__order_Otrans:(forall (B:a) (A:a) (C:a), (((less_eq B) A)->(((less_eq C) B)->((less_eq C) A)))). % 0.77/0.92 Axiom fact_67_local_Oeq__iff:(((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (X3:a) (Y4:a)=> ((and ((less_eq X3) Y4)) ((less_eq Y4) X3)))). % 0.77/0.92 Axiom fact_68_local_Oeq__refl:(forall (X:a) (Y:a), ((((eq a) X) Y)->((less_eq X) Y))). % 0.77/0.92 Axiom fact_69_local_Oord__eq__le__trans:(forall (A:a) (B:a) (C:a), ((((eq a) A) B)->(((less_eq B) C)->((less_eq A) C)))). % 0.77/0.92 Axiom fact_70_local_Oord__le__eq__trans:(forall (A:a) (B:a) (C:a), (((less_eq A) B)->((((eq a) B) C)->((less_eq A) C)))). % 0.77/0.92 Axiom fact_71_local_Oorder_Oantisym:(forall (A:a) (B:a), (((less_eq A) B)->(((less_eq B) A)->(((eq a) A) B)))). % 0.77/0.92 Axiom fact_72_local_Oorder_Oeq__iff:(((eq (a->(a->Prop))) (fun (Y3:a) (Z3:a)=> (((eq a) Y3) Z3))) (fun (A3:a) (B2:a)=> ((and ((less_eq A3) B2)) ((less_eq B2) A3)))). % 0.77/0.92 Axiom fact_73_local_Oorder_Otrans:(forall (A:a) (B:a) (C:a), (((less_eq A) B)->(((less_eq B) C)->((less_eq A) C)))). % 0.77/0.92 Axiom fact_74_local_Oorder__trans:(forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((less_eq Y) Z)->((less_eq X) Z)))). % 0.77/0.92 Axiom fact_75_local_Ole__infI2:(forall (B:a) (X:a) (A:a), (((less_eq B) X)->((less_eq ((inf A) B)) X))). % 0.77/0.92 Axiom fact_76_local_Ole__infI1:(forall (A:a) (X:a) (B:a), (((less_eq A) X)->((less_eq ((inf A) B)) X))). % 0.77/0.92 Axiom fact_77_local_Ole__infI:(forall (X:a) (A:a) (B:a), (((less_eq X) A)->(((less_eq X) B)->((less_eq X) ((inf A) B))))). % 0.77/0.92 Axiom fact_78_local_Ole__infE:(forall (X:a) (A:a) (B:a), (((less_eq X) ((inf A) B))->((((less_eq X) A)->(((less_eq X) B)->False))->False))). % 0.77/0.92 Axiom fact_79_local_Ole__iff__inf:(forall (X:a) (Y:a), (((eq Prop) ((less_eq X) Y)) (((eq a) ((inf X) Y)) X))). % 0.77/0.92 Axiom fact_80_local_Oinf__unique:(forall (F:(a->(a->a))) (X:a) (Y:a), ((forall (X2:a) (Y2:a), ((less_eq ((F X2) Y2)) X2))->((forall (X2:a) (Y2:a), ((less_eq ((F X2) Y2)) Y2))->((forall (X2:a) (Y2:a) (Z2:a), (((less_eq X2) Y2)->(((less_eq X2) Z2)->((less_eq X2) ((F Y2) Z2)))))->(((eq a) ((inf X) Y)) ((F X) Y)))))). % 0.77/0.92 Axiom fact_81_local_Oinf__mono:(forall (A:a) (C:a) (B:a) (D:a), (((less_eq A) C)->(((less_eq B) D)->((less_eq ((inf A) B)) ((inf C) D))))). % 0.77/0.92 Axiom fact_82_local_Oinf__le2:(forall (X:a) (Y:a), ((less_eq ((inf X) Y)) Y)). % 0.77/0.92 Axiom fact_83_local_Oinf__le1:(forall (X:a) (Y:a), ((less_eq ((inf X) Y)) X)). % 0.77/0.92 Axiom fact_84_local_Oinf__greatest:(forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((less_eq X) Z)->((less_eq X) ((inf Y) Z))))). % 0.77/0.92 Axiom fact_85_local_Oinf__absorb2:(forall (Y:a) (X:a), (((less_eq Y) X)->(((eq a) ((inf X) Y)) Y))). % 0.77/0.92 Axiom fact_86_local_Oinf__absorb1:(forall (X:a) (Y:a), (((less_eq X) Y)->(((eq a) ((inf X) Y)) X))). % 0.77/0.92 Axiom fact_87_local_Oinf_Oorder__iff:(forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) A) ((inf A) B)))). % 0.77/0.92 Axiom fact_88_local_Oinf_OorderI:(forall (A:a) (B:a), ((((eq a) A) ((inf A) B))->((less_eq A) B))). % 0.77/0.92 Axiom fact_89_local_Oinf_OorderE:(forall (A:a) (B:a), (((less_eq A) B)->(((eq a) A) ((inf A) B)))). % 0.77/0.92 Axiom fact_90_local_Oinf_OcoboundedI2:(forall (B:a) (C:a) (A:a), (((less_eq B) C)->((less_eq ((inf A) B)) C))). % 0.77/0.92 Axiom fact_91_local_Oinf_OcoboundedI1:(forall (A:a) (C:a) (B:a), (((less_eq A) C)->((less_eq ((inf A) B)) C))). % 0.77/0.93 Axiom fact_92_local_Oinf_Ocobounded2:(forall (A:a) (B:a), ((less_eq ((inf A) B)) B)). % 0.77/0.93 Axiom fact_93_local_Oinf_Ocobounded1:(forall (A:a) (B:a), ((less_eq ((inf A) B)) A)). % 0.77/0.93 Axiom fact_94_local_Oinf_OboundedI:(forall (A:a) (B:a) (C:a), (((less_eq A) B)->(((less_eq A) C)->((less_eq A) ((inf B) C))))). % 0.77/0.93 Axiom fact_95_local_Oinf_OboundedE:(forall (A:a) (B:a) (C:a), (((less_eq A) ((inf B) C))->((((less_eq A) B)->(((less_eq A) C)->False))->False))). % 0.77/0.93 Axiom fact_96_local_Oinf_Oabsorb__iff2:(forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) ((inf A) B)) B))). % 0.77/0.93 Axiom fact_97_local_Oinf_Oabsorb__iff1:(forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) ((inf A) B)) A))). % 0.77/0.93 Axiom fact_98_local_Oinf_Oabsorb2:(forall (B:a) (A:a), (((less_eq B) A)->(((eq a) ((inf A) B)) B))). % 0.77/0.93 Axiom fact_99_local_Oinf_Oabsorb1:(forall (A:a) (B:a), (((less_eq A) B)->(((eq a) ((inf A) B)) A))). % 0.77/0.93 Axiom fact_100_local_Osup__unique:(forall (F:(a->(a->a))) (X:a) (Y:a), ((forall (X2:a) (Y2:a), ((less_eq X2) ((F X2) Y2)))->((forall (X2:a) (Y2:a), ((less_eq Y2) ((F X2) Y2)))->((forall (X2:a) (Y2:a) (Z2:a), (((less_eq Y2) X2)->(((less_eq Z2) X2)->((less_eq ((F Y2) Z2)) X2))))->(((eq a) ((sup X) Y)) ((F X) Y)))))). % 0.77/0.93 Axiom fact_101_local_Osup__mono:(forall (A:a) (C:a) (B:a) (D:a), (((less_eq A) C)->(((less_eq B) D)->((less_eq ((sup A) B)) ((sup C) D))))). % 0.77/0.93 Axiom fact_102_local_Osup__least:(forall (Y:a) (X:a) (Z:a), (((less_eq Y) X)->(((less_eq Z) X)->((less_eq ((sup Y) Z)) X)))). % 0.77/0.93 Axiom fact_103_local_Osup__ge2:(forall (Y:a) (X:a), ((less_eq Y) ((sup X) Y))). % 0.77/0.93 Axiom fact_104_local_Osup__ge1:(forall (X:a) (Y:a), ((less_eq X) ((sup X) Y))). % 0.77/0.93 Axiom fact_105_local_Osup__absorb2:(forall (X:a) (Y:a), (((less_eq X) Y)->(((eq a) ((sup X) Y)) Y))). % 0.77/0.93 Axiom fact_106_local_Osup__absorb1:(forall (Y:a) (X:a), (((less_eq Y) X)->(((eq a) ((sup X) Y)) X))). % 0.77/0.93 Axiom fact_107_local_Osup_Oorder__iff:(forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) A) ((sup A) B)))). % 0.77/0.93 Axiom fact_108_local_Osup_OorderI:(forall (A:a) (B:a), ((((eq a) A) ((sup A) B))->((less_eq B) A))). % 0.77/0.93 Axiom fact_109_local_Osup_OorderE:(forall (B:a) (A:a), (((less_eq B) A)->(((eq a) A) ((sup A) B)))). % 0.77/0.93 Axiom fact_110_local_Osup_Omono:(forall (C:a) (A:a) (D:a) (B:a), (((less_eq C) A)->(((less_eq D) B)->((less_eq ((sup C) D)) ((sup A) B))))). % 0.77/0.93 Axiom fact_111_local_Osup_OcoboundedI2:(forall (C:a) (B:a) (A:a), (((less_eq C) B)->((less_eq C) ((sup A) B)))). % 0.77/0.93 Axiom fact_112_local_Osup_OcoboundedI1:(forall (C:a) (A:a) (B:a), (((less_eq C) A)->((less_eq C) ((sup A) B)))). % 0.77/0.93 Axiom fact_113_local_Osup_Ocobounded2:(forall (B:a) (A:a), ((less_eq B) ((sup A) B))). % 0.77/0.93 Axiom fact_114_local_Osup_Ocobounded1:(forall (A:a) (B:a), ((less_eq A) ((sup A) B))). % 0.77/0.93 Axiom fact_115_local_Osup_OboundedI:(forall (B:a) (A:a) (C:a), (((less_eq B) A)->(((less_eq C) A)->((less_eq ((sup B) C)) A)))). % 0.77/0.93 Axiom fact_116_local_Osup_OboundedE:(forall (B:a) (C:a) (A:a), (((less_eq ((sup B) C)) A)->((((less_eq B) A)->(((less_eq C) A)->False))->False))). % 0.77/0.93 Axiom fact_117_local_Osup_Oabsorb__iff2:(forall (A:a) (B:a), (((eq Prop) ((less_eq A) B)) (((eq a) ((sup A) B)) B))). % 0.77/0.93 Axiom fact_118_local_Osup_Oabsorb__iff1:(forall (B:a) (A:a), (((eq Prop) ((less_eq B) A)) (((eq a) ((sup A) B)) A))). % 0.77/0.93 Axiom fact_119_local_Osup_Oabsorb2:(forall (A:a) (B:a), (((less_eq A) B)->(((eq a) ((sup A) B)) B))). % 0.77/0.93 Axiom fact_120_local_Osup_Oabsorb1:(forall (B:a) (A:a), (((less_eq B) A)->(((eq a) ((sup A) B)) A))). % 0.77/0.93 Axiom fact_121_local_Ole__supI2:(forall (X:a) (B:a) (A:a), (((less_eq X) B)->((less_eq X) ((sup A) B)))). % 0.77/0.93 Axiom fact_122_local_Ole__supI1:(forall (X:a) (A:a) (B:a), (((less_eq X) A)->((less_eq X) ((sup A) B)))). % 0.77/0.93 Axiom fact_123_local_Ole__supI:(forall (A:a) (X:a) (B:a), (((less_eq A) X)->(((less_eq B) X)->((less_eq ((sup A) B)) X)))). % 0.77/0.93 Axiom fact_124_local_Ole__supE:(forall (A:a) (B:a) (X:a), (((less_eq ((sup A) B)) X)->((((less_eq A) X)->(((less_eq B) X)->False))->False))). % 0.77/0.93 Axiom fact_125_local_Ole__iff__sup:(forall (X:a) (Y:a), (((eq Prop) ((less_eq X) Y)) (((eq a) ((sup X) Y)) Y))). % 0.77/0.93 Axiom fact_126_local_Omodular:(forall (X:a) (Y:a) (Z:a), (((less_eq X) Y)->(((eq a) ((sup X) ((inf Y) Z))) ((inf Y) ((sup X) Z))))). % 0.77/0.93 Axiom fact_127_local_Odistrib__sup__le:(forall (X:a) (Y:a) (Z:a), ((less_eq ((sup X) ((inf Y) Z))) ((inf ((sup X) Y)) ((sup X) Z)))). % 0.77/0.93 Axiom fact_128_local_Odistrib__inf__le:(forall (X:a) (Y:a) (Z:a), ((less_eq ((sup ((inf X) Y)) ((inf X) Z))) ((inf X) ((sup Y) Z)))). % 0.77/0.93 Axiom fact_129_local_Oincomp__def:(forall (X:a) (Y:a), (((eq Prop) (((modula1727524044comp_a less_eq) X) Y)) ((and (((less_eq X) Y)->False)) (((less_eq Y) X)->False)))). % 0.77/0.93 Axiom fact_130_local_Oc__a:(forall (A:a) (B:a) (C:a), (((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) C) A) B))). % 0.77/0.93 Axiom fact_131_local_Oorder_Orefl:(forall (A:a), ((less_eq A) A)). % 0.77/0.93 Axiom fact_132_local_Oorder__refl:(forall (X:a), ((less_eq X) X)). % 0.77/0.93 Axiom fact_133_local_OGreatestI2__order:(forall (P:(a->Prop)) (X:a) (Q:(a->Prop)), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq Y2) X)))->((forall (X2:a), ((P X2)->((forall (Y5:a), ((P Y5)->((less_eq Y5) X2)))->(Q X2))))->(Q ((greatest_a less_eq) P)))))). % 0.77/0.93 Axiom fact_134_local_OGreatest__equality:(forall (P:(a->Prop)) (X:a), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq Y2) X)))->(((eq a) ((greatest_a less_eq) P)) X)))). % 0.77/0.93 Axiom fact_135_local_Omax__def:(forall (A:a) (B:a), ((and (((less_eq A) B)->(((eq a) (((max_a less_eq) A) B)) B))) ((((less_eq A) B)->False)->(((eq a) (((max_a less_eq) A) B)) A)))). % 0.77/0.93 Axiom fact_136_local_Omin__def:(forall (A:a) (B:a), ((and (((less_eq A) B)->(((eq a) (((min_a less_eq) A) B)) A))) ((((less_eq A) B)->False)->(((eq a) (((min_a less_eq) A) B)) B)))). % 0.77/0.93 Axiom fact_137_a__def__equiv:(forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula17988509_aux_a inf) sup) A) B) C)) ((inf ((sup A) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))). % 0.77/0.93 Axiom fact_138_c__def__equiv:(forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula581031071_aux_a inf) sup) A) B) C)) ((inf ((sup C) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))). % 0.77/0.93 Axiom fact_139_b__def__equiv:(forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) (((((modula1373251614_aux_a inf) sup) A) B) C)) ((inf ((sup B) (((((modula1936294176_aux_a inf) sup) A) B) C))) (((((modula1144073633_aux_a inf) sup) A) B) C))))). % 0.77/0.93 Axiom fact_140_c__meet__a__eq__d:(forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula581031071_aux_a inf) sup) A) B) C)) (((((modula17988509_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))). % 0.77/0.93 Axiom fact_141_a__meet__b__eq__d:(forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula17988509_aux_a inf) sup) A) B) C)) (((((modula1373251614_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))). % 0.77/0.93 Axiom fact_142_b__meet__c__eq__d:(forall (A:a) (B:a) (C:a), (((less_eq (((((modula1936294176_aux_a inf) sup) A) B) C)) (((((modula1144073633_aux_a inf) sup) A) B) C))->(((eq a) ((inf (((((modula1373251614_aux_a inf) sup) A) B) C)) (((((modula581031071_aux_a inf) sup) A) B) C))) (((((modula1936294176_aux_a inf) sup) A) B) C)))). % 0.77/0.93 Axiom fact_143_local_Ole__inf__iff:(forall (X:a) (Y:a) (Z:a), (((eq Prop) ((less_eq X) ((inf Y) Z))) ((and ((less_eq X) Y)) ((less_eq X) Z)))). % 0.77/0.93 Axiom fact_144_local_Oinf_Obounded__iff:(forall (A:a) (B:a) (C:a), (((eq Prop) ((less_eq A) ((inf B) C))) ((and ((less_eq A) B)) ((less_eq A) C)))). % 0.77/0.93 Axiom fact_145_local_Osup_Obounded__iff:(forall (B:a) (C:a) (A:a), (((eq Prop) ((less_eq ((sup B) C)) A)) ((and ((less_eq B) A)) ((less_eq C) A)))). % 0.77/0.93 Axiom fact_146_local_Ole__sup__iff:(forall (X:a) (Y:a) (Z:a), (((eq Prop) ((less_eq ((sup X) Y)) Z)) ((and ((less_eq X) Z)) ((less_eq Y) Z)))). % 0.77/0.93 Axiom fact_147_local_OLeast1I:(forall (P:(a->Prop)), (((ex a) (fun (X4:a)=> ((and ((and (P X4)) (forall (Y2:a), ((P Y2)->((less_eq X4) Y2))))) (forall (Y2:a), (((and (P Y2)) (forall (Ya:a), ((P Ya)->((less_eq Y2) Ya))))->(((eq a) Y2) X4))))))->(P ((least_a less_eq) P)))). % 0.77/0.93 Axiom fact_148_local_OLeast1__le:(forall (P:(a->Prop)) (Z:a), (((ex a) (fun (X4:a)=> ((and ((and (P X4)) (forall (Y2:a), ((P Y2)->((less_eq X4) Y2))))) (forall (Y2:a), (((and (P Y2)) (forall (Ya:a), ((P Ya)->((less_eq Y2) Ya))))->(((eq a) Y2) X4))))))->((P Z)->((less_eq ((least_a less_eq) P)) Z)))). % 0.77/0.93 Axiom fact_149_local_OLeastI2__order:(forall (P:(a->Prop)) (X:a) (Q:(a->Prop)), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq X) Y2)))->((forall (X2:a), ((P X2)->((forall (Y5:a), ((P Y5)->((less_eq X2) Y5)))->(Q X2))))->(Q ((least_a less_eq) P)))))). % 0.77/0.93 Axiom fact_150_local_OLeast__equality:(forall (P:(a->Prop)) (X:a), ((P X)->((forall (Y2:a), ((P Y2)->((less_eq X) Y2)))->(((eq a) ((least_a less_eq) P)) X)))). % 0.77/0.93 Axiom fact_151_lattice_Oc__aux_Ocong:(((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula581031071_aux_a) modula581031071_aux_a). % 0.77/0.93 Axiom fact_152_lattice_Ob__aux_Ocong:(((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula1373251614_aux_a) modula1373251614_aux_a). % 0.77/0.93 Axiom fact_153_lattice_Oa__aux_Ocong:(((eq ((a->(a->a))->((a->(a->a))->(a->(a->(a->a)))))) modula17988509_aux_a) modula17988509_aux_a). % 0.77/0.93 Axiom fact_154_abel__semigroup_Oaxioms_I1_J:(forall (F:(a->(a->a))), ((abel_semigroup_a F)->(semigroup_a F))). % 0.77/0.93 Axiom fact_155_semilattice__set__def:(((eq ((a->(a->a))->Prop)) lattic1885654924_set_a) semilattice_a). % 0.77/0.93 Axiom fact_156_semilattice__set_Ointro:(forall (F:(a->(a->a))), ((semilattice_a F)->(lattic1885654924_set_a F))). % 0.77/0.93 Axiom fact_157_semilattice__set_Oaxioms:(forall (F:(a->(a->a))), ((lattic1885654924_set_a F)->(semilattice_a F))). % 0.77/0.93 Axiom fact_158_semilattice_Oaxioms_I1_J:(forall (F:(a->(a->a))), ((semilattice_a F)->(abel_semigroup_a F))). % 0.77/0.93 Axiom fact_159_local_Obdd__above__def:(forall (A2:set_a), (((eq Prop) ((condit1627435690bove_a less_eq) A2)) ((ex a) (fun (M:a)=> (forall (X3:a), (((member_a X3) A2)->((less_eq X3) M))))))). % 0.77/0.93 Axiom fact_160_local_Obdd__below__def:(forall (A2:set_a), (((eq Prop) ((condit1001553558elow_a less_eq) A2)) ((ex a) (fun (M2:a)=> (forall (X3:a), (((member_a X3) A2)->((less_eq M2) X3))))))). % 0.77/0.93 Axiom fact_161_local_Obdd__belowI:(forall (A2:set_a) (M3:a), ((forall (X2:a), (((member_a X2) A2)->((less_eq M3) X2)))->((condit1001553558elow_a less_eq) A2))). % 0.77/0.93 Axiom fact_162_local_Obdd__aboveI:(forall (A2:set_a) (M4:a), ((forall (X2:a), (((member_a X2) A2)->((less_eq X2) M4)))->((condit1627435690bove_a less_eq) A2))). % 0.77/0.93 Axiom fact_163_lattice_Oincomp_Ocong:(((eq ((a->(a->Prop))->(a->(a->Prop)))) modula1727524044comp_a) modula1727524044comp_a). % 0.77/0.93 Axiom fact_164_abel__semigroup_Oleft__commute:(forall (F:(a->(a->a))) (B:a) (A:a) (C:a), ((abel_semigroup_a F)->(((eq a) ((F B) ((F A) C))) ((F A) ((F B) C))))). % 0.77/0.93 Axiom fact_165_semilattice_Oright__idem:(forall (F:(a->(a->a))) (A:a) (B:a), ((semilattice_a F)->(((eq a) ((F ((F A) B)) B)) ((F A) B)))). % 0.77/0.93 Axiom fact_166_semilattice_Oleft__idem:(forall (F:(a->(a->a))) (A:a) (B:a), ((semilattice_a F)->(((eq a) ((F A) ((F A) B))) ((F A) B)))). % 0.77/0.93 Axiom fact_167_abel__semigroup_Ocommute:(forall (F:(a->(a->a))) (A:a) (B:a), ((abel_semigroup_a F)->(((eq a) ((F A) B)) ((F B) A)))). % 0.77/0.93 Axiom fact_168_semilattice_Oidem:(forall (F:(a->(a->a))) (A:a), ((semilattice_a F)->(((eq a) ((F A) A)) A))). % 0.77/0.93 Axiom fact_169_semigroup_Ointro:(forall (F:(a->(a->a))), ((forall (A4:a) (B3:a) (C2:a), (((eq a) ((F ((F A4) B3)) C2)) ((F A4) ((F B3) C2))))->(semigroup_a F))). % 0.77/0.93 Axiom fact_170_semigroup_Oassoc:(forall (F:(a->(a->a))) (A:a) (B:a) (C:a), ((semigroup_a F)->(((eq a) ((F ((F A) B)) C)) ((F A) ((F B) C))))). % 0.77/0.93 Axiom fact_171_semigroup__def:(((eq ((a->(a->a))->Prop)) semigroup_a) (fun (F2:(a->(a->a)))=> (forall (A3:a) (B2:a) (C3:a), (((eq a) ((F2 ((F2 A3) B2)) C3)) ((F2 A3) ((F2 B2) C3)))))). % 0.77/0.93 Axiom fact_172_local_Obdd__below__mono:(forall (B4:set_a) (A2:set_a), (((condit1001553558elow_a less_eq) B4)->(((ord_less_eq_set_a A2) B4)->((condit1001553558elow_a less_eq) A2)))). % 0.77/0.93 Axiom fact_173_local_Obdd__above__mono:(forall (B4:set_a) (A2:set_a), (((condit1627435690bove_a less_eq) B4)->(((ord_less_eq_set_a A2) B4)->((condit1627435690bove_a less_eq) A2)))). % 0.77/0.93 Axiom fact_174_local_Obdd__below__finite:(forall (A2:set_a), ((finite_finite_a A2)->((condit1001553558elow_a less_eq) A2))). % 0.77/0.93 Axiom fact_175_local_Ofinite__has__maximal2:(forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((ex a) (fun (X2:a)=> ((and ((and ((member_a X2) A2)) ((less_eq A) X2))) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq X2) Xa)->(((eq a) X2) Xa)))))))))). % 0.77/0.93 Axiom fact_176_local_Ofinite__has__minimal2:(forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((ex a) (fun (X2:a)=> ((and ((and ((member_a X2) A2)) ((less_eq X2) A))) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq Xa) X2)->(((eq a) X2) Xa)))))))))). % 0.77/0.93 Axiom fact_177_local_Obdd__above__finite:(forall (A2:set_a), ((finite_finite_a A2)->((condit1627435690bove_a less_eq) A2))). % 0.77/0.93 Axiom fact_178_local_OantimonoD:(forall (F:(a->set_a)) (X:a) (Y:a), (((antimono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F Y)) (F X))))). % 0.77/0.93 Axiom fact_179_local_OantimonoE:(forall (F:(a->set_a)) (X:a) (Y:a), (((antimono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F Y)) (F X))))). % 0.77/0.93 Axiom fact_180_local_OantimonoI:(forall (F:(a->set_a)), ((forall (X2:a) (Y2:a), (((less_eq X2) Y2)->((ord_less_eq_set_a (F Y2)) (F X2))))->((antimono_a_set_a less_eq) F))). % 0.77/0.93 Axiom fact_181_local_Oantimono__def:(forall (F:(a->set_a)), (((eq Prop) ((antimono_a_set_a less_eq) F)) (forall (X3:a) (Y4:a), (((less_eq X3) Y4)->((ord_less_eq_set_a (F Y4)) (F X3)))))). % 0.77/0.93 Axiom fact_182_local_Omono__def:(forall (F:(a->set_a)), (((eq Prop) ((mono_a_set_a less_eq) F)) (forall (X3:a) (Y4:a), (((less_eq X3) Y4)->((ord_less_eq_set_a (F X3)) (F Y4)))))). % 0.77/0.93 Axiom fact_183_local_OmonoI:(forall (F:(a->set_a)), ((forall (X2:a) (Y2:a), (((less_eq X2) Y2)->((ord_less_eq_set_a (F X2)) (F Y2))))->((mono_a_set_a less_eq) F))). % 0.77/0.93 Axiom fact_184_local_OmonoE:(forall (F:(a->set_a)) (X:a) (Y:a), (((mono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F X)) (F Y))))). % 0.77/0.93 Axiom fact_185_local_OmonoD:(forall (F:(a->set_a)) (X:a) (Y:a), (((mono_a_set_a less_eq) F)->(((less_eq X) Y)->((ord_less_eq_set_a (F X)) (F Y))))). % 0.77/0.93 Axiom fact_186_local_OSup__fin_OcoboundedI:(forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((less_eq A) ((lattic1781219155_fin_a sup) A2))))). % 0.77/0.93 Axiom fact_187_local_OInf__fin_OcoboundedI:(forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->((less_eq ((lattic247676691_fin_a inf) A2)) A)))). % 0.77/0.93 Axiom fact_188_local_OSup__fin_Oin__idem:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->(((member_a X) A2)->(((eq a) ((sup X) ((lattic1781219155_fin_a sup) A2))) ((lattic1781219155_fin_a sup) A2))))). % 0.77/0.93 Axiom fact_189_local_OInf__fin_Oin__idem:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->(((member_a X) A2)->(((eq a) ((inf X) ((lattic247676691_fin_a inf) A2))) ((lattic247676691_fin_a inf) A2))))). % 0.77/0.93 Axiom fact_190_local_Osup__Inf__absorb:(forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->(((eq a) ((sup ((lattic247676691_fin_a inf) A2)) A)) A)))). % 0.77/0.93 Axiom fact_191_local_Oinf__Sup__absorb:(forall (A2:set_a) (A:a), ((finite_finite_a A2)->(((member_a A) A2)->(((eq a) ((inf A) ((lattic1781219155_fin_a sup) A2))) A)))). % 0.77/0.93 Axiom fact_192_semilattice__inf_OInf__fin_Ocong:(((eq ((a->(a->a))->(set_a->a))) lattic247676691_fin_a) lattic247676691_fin_a). % 0.77/0.93 Axiom fact_193_semilattice__sup_OSup__fin_Ocong:(((eq ((a->(a->a))->(set_a->a))) lattic1781219155_fin_a) lattic1781219155_fin_a). % 0.77/0.93 Axiom fact_194_local_OInf__fin__le__Sup__fin:(forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((less_eq ((lattic247676691_fin_a inf) A2)) ((lattic1781219155_fin_a sup) A2))))). % 0.77/0.93 Axiom fact_195_local_OSup__fin_Osubset__imp:(forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->((not (((eq set_a) A2) bot_bot_set_a))->((finite_finite_a B4)->((less_eq ((lattic1781219155_fin_a sup) A2)) ((lattic1781219155_fin_a sup) B4)))))). % 0.77/0.93 Axiom fact_196_local_Ofinite__has__minimal:(forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((ex a) (fun (X2:a)=> ((and ((member_a X2) A2)) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq Xa) X2)->(((eq a) X2) Xa)))))))))). % 0.77/0.93 Axiom fact_197_local_Ofinite__has__maximal:(forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((ex a) (fun (X2:a)=> ((and ((member_a X2) A2)) (forall (Xa:a), (((member_a Xa) A2)->(((less_eq X2) Xa)->(((eq a) X2) Xa)))))))))). % 0.77/0.93 Axiom fact_198_local_OInf__fin_Osubset:(forall (A2:set_a) (B4:set_a), ((finite_finite_a A2)->((not (((eq set_a) B4) bot_bot_set_a))->(((ord_less_eq_set_a B4) A2)->(((eq a) ((inf ((lattic247676691_fin_a inf) B4)) ((lattic247676691_fin_a inf) A2))) ((lattic247676691_fin_a inf) A2)))))). % 0.77/0.93 Axiom fact_199_local_OSup__fin_Osubset:(forall (A2:set_a) (B4:set_a), ((finite_finite_a A2)->((not (((eq set_a) B4) bot_bot_set_a))->(((ord_less_eq_set_a B4) A2)->(((eq a) ((sup ((lattic1781219155_fin_a sup) B4)) ((lattic1781219155_fin_a sup) A2))) ((lattic1781219155_fin_a sup) A2)))))). % 0.77/0.93 Axiom fact_200_local_OInf__fin_Obounded__iff:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq Prop) ((less_eq X) ((lattic247676691_fin_a inf) A2))) (forall (X3:a), (((member_a X3) A2)->((less_eq X) X3))))))). % 0.77/0.93 Axiom fact_201_local_OInf__fin_OboundedI:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (A4:a), (((member_a A4) A2)->((less_eq X) A4)))->((less_eq X) ((lattic247676691_fin_a inf) A2)))))). % 0.77/0.93 Axiom fact_202_local_OInf__fin_OboundedE:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((less_eq X) ((lattic247676691_fin_a inf) A2))->(forall (A5:a), (((member_a A5) A2)->((less_eq X) A5))))))). % 0.77/0.93 Axiom fact_203_local_OSup__fin_Obounded__iff:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq Prop) ((less_eq ((lattic1781219155_fin_a sup) A2)) X)) (forall (X3:a), (((member_a X3) A2)->((less_eq X3) X))))))). % 0.77/0.93 Axiom fact_204_local_OSup__fin_OboundedI:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (A4:a), (((member_a A4) A2)->((less_eq A4) X)))->((less_eq ((lattic1781219155_fin_a sup) A2)) X))))). % 0.77/0.93 Axiom fact_205_local_OSup__fin_OboundedE:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->(((less_eq ((lattic1781219155_fin_a sup) A2)) X)->(forall (A5:a), (((member_a A5) A2)->((less_eq A5) X))))))). % 0.77/0.93 Axiom fact_206_local_OInf__fin_Osubset__imp:(forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->((not (((eq set_a) A2) bot_bot_set_a))->((finite_finite_a B4)->((less_eq ((lattic247676691_fin_a inf) B4)) ((lattic247676691_fin_a inf) A2)))))). % 0.77/0.93 Axiom fact_207_local_Obdd__above__empty:((condit1627435690bove_a less_eq) bot_bot_set_a). % 0.77/0.93 Axiom fact_208_local_Obdd__below__empty:((condit1001553558elow_a less_eq) bot_bot_set_a). % 0.77/0.93 Axiom fact_209_local_Onot__empty__eq__Iic__eq__empty:(forall (H:a), (not (((eq set_a) bot_bot_set_a) ((set_atMost_a less_eq) H)))). % 0.77/0.93 Axiom fact_210_local_Onot__empty__eq__Ici__eq__empty:(forall (L:a), (not (((eq set_a) bot_bot_set_a) ((set_atLeast_a less_eq) L)))). % 0.77/0.93 Axiom fact_211_local_OatLeast__iff:(forall (_TPTP_I:a) (K:a), (((eq Prop) ((member_a _TPTP_I) ((set_atLeast_a less_eq) K))) ((less_eq K) _TPTP_I))). % 0.77/0.93 Axiom fact_212_local_OatMost__iff:(forall (_TPTP_I:a) (K:a), (((eq Prop) ((member_a _TPTP_I) ((set_atMost_a less_eq) K))) ((less_eq _TPTP_I) K))). % 0.77/0.93 Axiom fact_213_local_Obdd__below__Ici:(forall (A:a), ((condit1001553558elow_a less_eq) ((set_atLeast_a less_eq) A))). % 0.77/0.93 Axiom fact_214_local_Obdd__above__Iic:(forall (B:a), ((condit1627435690bove_a less_eq) ((set_atMost_a less_eq) B))). % 0.77/0.93 Axiom fact_215_empty__subsetI:(forall (A2:set_a), ((ord_less_eq_set_a bot_bot_set_a) A2)). % 0.77/0.93 Axiom fact_216_subset__empty:(forall (A2:set_a), (((eq Prop) ((ord_less_eq_set_a A2) bot_bot_set_a)) (((eq set_a) A2) bot_bot_set_a))). % 0.77/0.93 Axiom fact_217_empty__iff:(forall (C:a), (((member_a C) bot_bot_set_a)->False)). % 0.77/0.93 Axiom fact_218_all__not__in__conv:(forall (A2:set_a), (((eq Prop) (forall (X3:a), (((member_a X3) A2)->False))) (((eq set_a) A2) bot_bot_set_a))). % 0.77/0.93 Axiom fact_219_Collect__empty__eq:(forall (P:(a->Prop)), (((eq Prop) (((eq set_a) (collect_a P)) bot_bot_set_a)) (forall (X3:a), ((P X3)->False)))). % 0.77/0.93 Axiom fact_220_empty__Collect__eq:(forall (P:(a->Prop)), (((eq Prop) (((eq set_a) bot_bot_set_a) (collect_a P))) (forall (X3:a), ((P X3)->False)))). % 0.77/0.93 Axiom fact_221_subsetI:(forall (A2:set_a) (B4:set_a), ((forall (X2:a), (((member_a X2) A2)->((member_a X2) B4)))->((ord_less_eq_set_a A2) B4))). % 0.77/0.93 Axiom fact_222_subset__antisym:(forall (A2:set_a) (B4:set_a), (((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) A2)->(((eq set_a) A2) B4)))). % 0.77/0.93 Axiom fact_223_emptyE:(forall (A:a), (((member_a A) bot_bot_set_a)->False)). % 0.77/0.93 Axiom fact_224_equals0D:(forall (A2:set_a) (A:a), ((((eq set_a) A2) bot_bot_set_a)->(((member_a A) A2)->False))). % 0.77/0.93 Axiom fact_225_equals0I:(forall (A2:set_a), ((forall (Y2:a), (((member_a Y2) A2)->False))->(((eq set_a) A2) bot_bot_set_a))). % 0.77/0.93 Axiom fact_226_ex__in__conv:(forall (A2:set_a), (((eq Prop) ((ex a) (fun (X3:a)=> ((member_a X3) A2)))) (not (((eq set_a) A2) bot_bot_set_a)))). % 0.77/0.93 Axiom fact_227_in__mono:(forall (A2:set_a) (B4:set_a) (X:a), (((ord_less_eq_set_a A2) B4)->(((member_a X) A2)->((member_a X) B4)))). % 0.77/0.93 Axiom fact_228_subsetD:(forall (A2:set_a) (B4:set_a) (C:a), (((ord_less_eq_set_a A2) B4)->(((member_a C) A2)->((member_a C) B4)))). % 0.77/0.93 Axiom fact_229_equalityE:(forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) A2)->False))->False))). % 0.77/0.93 Axiom fact_230_subset__eq:(((eq (set_a->(set_a->Prop))) ord_less_eq_set_a) (fun (A6:set_a) (B5:set_a)=> (forall (X3:a), (((member_a X3) A6)->((member_a X3) B5))))). % 0.77/0.93 Axiom fact_231_equalityD1:(forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((ord_less_eq_set_a A2) B4))). % 0.77/0.93 Axiom fact_232_equalityD2:(forall (A2:set_a) (B4:set_a), ((((eq set_a) A2) B4)->((ord_less_eq_set_a B4) A2))). % 0.77/0.96 Axiom fact_233_subset__iff:(((eq (set_a->(set_a->Prop))) ord_less_eq_set_a) (fun (A6:set_a) (B5:set_a)=> (forall (T:a), (((member_a T) A6)->((member_a T) B5))))). % 0.77/0.96 Axiom fact_234_subset__refl:(forall (A2:set_a), ((ord_less_eq_set_a A2) A2)). % 0.77/0.96 Axiom fact_235_Collect__mono:(forall (P:(a->Prop)) (Q:(a->Prop)), ((forall (X2:a), ((P X2)->(Q X2)))->((ord_less_eq_set_a (collect_a P)) (collect_a Q)))). % 0.77/0.96 Axiom fact_236_subset__trans:(forall (A2:set_a) (B4:set_a) (C4:set_a), (((ord_less_eq_set_a A2) B4)->(((ord_less_eq_set_a B4) C4)->((ord_less_eq_set_a A2) C4)))). % 0.77/0.96 Axiom fact_237_set__eq__subset:(((eq (set_a->(set_a->Prop))) (fun (Y3:set_a) (Z3:set_a)=> (((eq set_a) Y3) Z3))) (fun (A6:set_a) (B5:set_a)=> ((and ((ord_less_eq_set_a A6) B5)) ((ord_less_eq_set_a B5) A6)))). % 0.77/0.96 Axiom fact_238_Collect__mono__iff:(forall (P:(a->Prop)) (Q:(a->Prop)), (((eq Prop) ((ord_less_eq_set_a (collect_a P)) (collect_a Q))) (forall (X3:a), ((P X3)->(Q X3))))). % 0.77/0.96 Axiom fact_239_local_Omono__inf:(forall (F:(a->set_a)) (A2:a) (B4:a), (((mono_a_set_a less_eq) F)->((ord_less_eq_set_a (F ((inf A2) B4))) ((inf_inf_set_a (F A2)) (F B4))))). % 0.77/0.96 Axiom fact_240_local_OSup__fin_Oinsert__not__elem:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((((member_a X) A2)->False)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq a) ((lattic1781219155_fin_a sup) ((insert_a X) A2))) ((sup X) ((lattic1781219155_fin_a sup) A2))))))). % 0.77/0.96 Axiom fact_241_local_Obdd__below__Int2:(forall (B4:set_a) (A2:set_a), (((condit1001553558elow_a less_eq) B4)->((condit1001553558elow_a less_eq) ((inf_inf_set_a A2) B4)))). % 0.77/0.96 Axiom fact_242_local_Obdd__below__Int1:(forall (A2:set_a) (B4:set_a), (((condit1001553558elow_a less_eq) A2)->((condit1001553558elow_a less_eq) ((inf_inf_set_a A2) B4)))). % 0.77/0.96 Axiom fact_243_local_Obdd__above__Int2:(forall (B4:set_a) (A2:set_a), (((condit1627435690bove_a less_eq) B4)->((condit1627435690bove_a less_eq) ((inf_inf_set_a A2) B4)))). % 0.77/0.96 Axiom fact_244_local_Obdd__above__Int1:(forall (A2:set_a) (B4:set_a), (((condit1627435690bove_a less_eq) A2)->((condit1627435690bove_a less_eq) ((inf_inf_set_a A2) B4)))). % 0.77/0.96 Axiom fact_245_Int__subset__iff:(forall (C4:set_a) (A2:set_a) (B4:set_a), (((eq Prop) ((ord_less_eq_set_a C4) ((inf_inf_set_a A2) B4))) ((and ((ord_less_eq_set_a C4) A2)) ((ord_less_eq_set_a C4) B4)))). % 0.77/0.96 Axiom fact_246_semilattice__inf__class_Oinf_Oidem:(forall (A:set_a), (((eq set_a) ((inf_inf_set_a A) A)) A)). % 0.77/0.96 Axiom fact_247_semilattice__inf__class_Oinf__idem:(forall (X:set_a), (((eq set_a) ((inf_inf_set_a X) X)) X)). % 0.77/0.96 Axiom fact_248_semilattice__inf__class_Oinf_Oleft__idem:(forall (A:set_a) (B:set_a), (((eq set_a) ((inf_inf_set_a A) ((inf_inf_set_a A) B))) ((inf_inf_set_a A) B))). % 0.77/0.96 Axiom fact_249_semilattice__inf__class_Oinf__left__idem:(forall (X:set_a) (Y:set_a), (((eq set_a) ((inf_inf_set_a X) ((inf_inf_set_a X) Y))) ((inf_inf_set_a X) Y))). % 0.77/0.96 Axiom fact_250_semilattice__inf__class_Oinf_Oright__idem:(forall (A:set_a) (B:set_a), (((eq set_a) ((inf_inf_set_a ((inf_inf_set_a A) B)) B)) ((inf_inf_set_a A) B))). % 0.77/0.96 Axiom fact_251_semilattice__inf__class_Oinf__right__idem:(forall (X:set_a) (Y:set_a), (((eq set_a) ((inf_inf_set_a ((inf_inf_set_a X) Y)) Y)) ((inf_inf_set_a X) Y))). % 0.77/0.96 Axiom fact_252_local_OInf__fin_Oclosed:(forall (A2:set_a), ((finite_finite_a A2)->((not (((eq set_a) A2) bot_bot_set_a))->((forall (X2:a) (Y2:a), ((member_a ((inf X2) Y2)) ((insert_a X2) ((insert_a Y2) bot_bot_set_a))))->((member_a ((lattic247676691_fin_a inf) A2)) A2))))). % 0.77/0.96 Axiom fact_253_local_OInf__fin_Oinsert__not__elem:(forall (A2:set_a) (X:a), ((finite_finite_a A2)->((((member_a X) A2)->False)->((not (((eq set_a) A2) bot_bot_set_a))->(((eq a) ((lattic247676691_fin_a inf) ((insert_a X) A2))) ((inf X) ((lattic247676691_fin_a inf) A2))))))). % 0.77/0.96 Trying to prove (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 123.02/123.29 Found fact_82_local_Oinf__le200:=(fact_82_local_Oinf__le20 (((((modula1144073633_aux_a inf) sup) a2) b) c)):((less_eq ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) % 123.02/123.29 Found (fact_82_local_Oinf__le20 (((((modula1144073633_aux_a inf) sup) a2) b) c)) as proof of ((less_eq ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) % 123.02/123.29 Found ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) as proof of ((less_eq ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) % 123.02/123.29 Found ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) as proof of ((less_eq ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) % 123.02/123.29 Found (fact_126_local_Omodular000 ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) as proof of (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 123.02/123.29 Found ((fact_126_local_Omodular00 ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) as proof of (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 123.02/123.29 Found (((fact_126_local_Omodular0 (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) as proof of (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 123.02/123.29 Found ((((fact_126_local_Omodular ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) as proof of (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 124.01/124.21 Found ((((fact_126_local_Omodular ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) as proof of (((eq a) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) ((inf (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))))) % 124.01/124.21 Got proof ((((fact_126_local_Omodular ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) % 124.01/124.21 Time elapsed = 122.334320s % 124.01/124.21 node=6890 cost=247.000000 depth=7 % 124.01/124.21:::::::::::::::::::::: % 124.01/124.21 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 124.01/124.21 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p % 124.01/124.21 ((((fact_126_local_Omodular ((inf ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c)) ((sup a2) (((((modula1936294176_aux_a inf) sup) a2) b) c))) ((fact_82_local_Oinf__le2 ((sup b) (((((modula1936294176_aux_a inf) sup) a2) b) c))) (((((modula1144073633_aux_a inf) sup) a2) b) c))) % 124.01/124.21 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------