DR_eq_DC_or_EC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "DR_eq_DC_or_EC", "DR_def", "DC_def", "O_impl_C",
                     "EC_def"
        Prover: SPASS

PP_eq_TPP_or_NTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "PP_eq_TPP_or_NTPP", "NTPP_def",
                     "ga_non_empty_sort_Reg", "TPP_def"
        Prover: SPASS

PPi_eq_TPPi_or_NTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "PPi_eq_TPPi_or_NTPPi", "PPi_def", "NTPPi_def",
                     "TPPi_def", "PP_eq_TPP_or_NTPP"
        Prover: SPASS

?_RCC8
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "?_RCC8", "?_RCC5", "?_RCC8_def", "DR_eq_DC_or_EC",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "?_RCC5_def"
        Prover: SPASS

?_RCC5_RCC8
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "?_RCC5_RCC8", "?_RCC5", "?_RCC8"
        Prover: SPASS

sym_DC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "sym_DC", "DC_def", "C_sym"
        Prover: SPASS

sym_EC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "sym_EC", "C_sym", "sym_DR", "EC_def",
                     "DR_eq_DC_or_EC", "DC_def"
        Prover: SPASS

disj_DC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_DC", "Ax1", "DR_def", "O_impl_C", "P_impl_O",
                     "EQ_def", "PPi_def", "PO_def", "PP_def", "sym_DR", "EC_def",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "sym_DC", "disj_DR",
                     "DC_def", "P_def", "ga_non_empty_sort_QReg"
        Prover: SPASS

disj_EC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_EC", "P_impl_O", "O_sym", "EQ_def", "PPi_def",
                     "PP_def", "sym_DR", "TPPi_def", "DR_eq_DC_or_EC",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "sym_EC", "disj_DR",
                     "EC_def", "disj_DC"
        Prover: SPASS

disj_TPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_TPP", "TPP_def", "ga_non_empty_sort_Reg",
                     "P_impl_O", "O_sym", "PPi_def", "PP_def", "sym_PO", "sym_DR",
                     "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "DR_def", "disj_PP", "disj_PO", "disj_EC",
                     "NTPP_def"
        Prover: SPASS

disj_NTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_NTPP", "PPi_def", "sym_PO", "NTPPi_def",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "disj_PP", "disj_PO",
                     "disj_DC", "disj_EC", "disj_TPP"
        Prover: SPASS

disj_TPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_TPPi", "EQ_def", "sym_PO", "NTPPi_def",
                     "TPPi_def", "sym_EC", "disj_DC", "disj_TPP", "disj_NTPP"
        Prover: SPASS

disj_NTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_NTPPi", "EQ_def", "sym_PO", "NTPPi_def",
                     "disj_DC", "disj_EC", "disj_TPP", "disj_NTPP", "disj_TPPi"
        Prover: SPASS

cmps_DCDC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCDC", "?_RCC8"
        Prover: SPASS

cmps_DCEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCEC", "?_RCC5", "EQ_def", "PPi_def", "PP_def",
                     "sym_PO", "sym_DR", "TPPi_def", "EC_def", "DR_eq_DC_or_EC",
                     "PPi_eq_TPPi_or_NTPPi", "sym_DC", "sym_EC", "DC_def", "disj_EC",
                     "PP_eq_TPP_or_NTPP", "P_def", "ga_non_empty_sort_QReg",
                     "?_RCC5_def"
        Prover: SPASS

cmps_DCPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCPO", "?_RCC5", "C_sym", "O_impl_C", "EQ_def",
                     "PPi_def", "PO_def", "PP_def", "sym_PO", "sym_DR", "TPPi_def",
                     "DR_eq_DC_or_EC", "PPi_eq_TPPi_or_NTPPi", "sym_DC", "sym_EC",
                     "DC_def", "disj_DC", "PP_eq_TPP_or_NTPP", "P_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_DCTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCTPP", "?_RCC5", "O_impl_C", "P_impl_O",
                     "O_sym", "EQ_def", "PPi_def", "PP_def", "sym_PO", "sym_DR",
                     "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "sym_DC", "DR_def", "DC_def", "P_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_DCNTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCNTPP", "?_RCC5", "O_impl_C", "P_impl_O",
                     "EQ_def", "PPi_def", "PP_def", "sym_PO", "sym_DR", "NTPPi_def",
                     "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "sym_DC", "sym_EC", "DC_def", "disj_NTPPi",
                     "P_def", "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_DCTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCTPPi", "DC_def", "P_impl_O", "PP_def",
                     "TPPi_def", "PP_eq_TPP_or_NTPP", "disj_TPP", "PO_def", "P_def",
                     "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_DCNTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DCNTPPi", "DC_def", "PPi_def", "PP_def",
                     "PPi_eq_TPPi_or_NTPPi", "P_def", "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_ECDC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECDC", "?_RCC5", "C_sym", "EQ_def", "PP_def",
                     "EC_def", "sym_DC", "DC_def", "DR_eq_DC_or_EC",
                     "PPi_eq_TPPi_or_NTPPi", "P_def", "ga_non_empty_sort_QReg",
                     "?_RCC5_def"
        Prover: SPASS

cmps_ECEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECEC", "?_RCC5", "NTPPi_def", "sym_EC",
                     "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi",
                     "NTPP_def", "ga_non_empty_sort_Reg", "?_RCC5_def"
        Prover: SPASS

cmps_ECPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECPO", "?_RCC5", "EQ_def", "PPi_def", "PO_def",
                     "sym_PO", "sym_DR", "TPPi_def", "DR_eq_DC_or_EC",
                     "PPi_eq_TPPi_or_NTPPi", "sym_EC", "DR_def", "PP_eq_TPP_or_NTPP",
                     "cmps_PPDR", "cmps_EQDR", "?_RCC5_def"
        Prover: SPASS

cmps_ECTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECTPP", "?_RCC5", "P_impl_O", "O_sym", "EQ_def",
                     "PPi_def", "PP_def", "sym_PO", "sym_DR", "TPPi_def", "EC_def",
                     "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi",
                     "DR_def", "DC_def", "disj_TPP", "PO_def", "cmps_PPDR", "cmps_EQDR",
                     "P_def", "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_ECNTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECNTPP", "?_RCC5", "DC_def", "P_impl_O",
                     "O_sym", "EQ_def", "PPi_def", "PP_def", "sym_PO", "TPPi_def",
                     "EC_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "sym_DC", "sym_EC", "DR_def", "disj_PP",
                     "disj_NTPP", "PO_def", "cmps_PPDR", "cmps_EQDR", "P_def",
                     "ga_non_empty_sort_QReg", "NTPP_def", "ga_non_empty_sort_Reg",
                     "?_RCC5_def"
        Prover: SPASS

cmps_ECTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECTPPi", "DR_eq_DC_or_EC",
                     "PPi_eq_TPPi_or_NTPPi", "cmps_DRPPi"
        Prover: SPASS

cmps_ECNTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_ECNTPPi", "Ax1", "DR_def", "DC_def", "P_impl_O",
                     "O_sym", "PPi_def", "PP_def", "sym_DR", "NTPPi_def",
                     "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi",
                     "PO_def", "EC_def", "cmps_PPDR", "P_inh_O", "NTP_def",
                     "ga_non_empty_sort_QReg", "NTPP_def", "ga_non_empty_sort_Reg"
        Prover: SPASS

cmps_PODC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PODC", "?_RCC5", "O_impl_C", "O_sym", "EQ_def",
                     "PO_def", "PP_def", "sym_DC", "DC_def", "disj_DC",
                     "DR_eq_DC_or_EC", "PPi_eq_TPPi_or_NTPPi", "cmps_EQPO", "P_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_POEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POEC", "?_RCC5", "O_sym", "PO_def", "PP_def",
                     "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP", "sym_EC", "DR_def",
                     "PPi_eq_TPPi_or_NTPPi", "cmps_EQDR", "P_inh_O", "?_RCC5_def"
        Prover: SPASS

cmps_POTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POTPP", "P_impl_O", "O_sym", "PO_def", "PP_def",
                     "TPPi_def", "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "DR_def",
                     "disj_PP", "disj_PO", "cmps_PP", "P_inh_O", "cmps_PPPO"
        Prover: SPASS

cmps_PONTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PONTPP", "?_RCC5", "P_impl_O", "O_sym",
                     "EQ_def", "PPi_def", "PO_def", "PP_def", "NTPPi_def", "TPPi_def",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "DR_def", "disj_PP",
                     "disj_PO", "disj_NTPPi", "P_inh_O", "?_RCC5_def", "cmps_PPPO"
        Prover: SPASS

cmps_POTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POTPPi", "?_RCC5", "EQ_def", "PPi_def",
                     "TPPi_def", "disj_TPP", "disj_TPPi", "disj_NTPPi",
                     "DR_eq_DC_or_EC", "PPi_eq_TPPi_or_NTPPi", "cmps_PPiPO",
                     "?_RCC5_def"
        Prover: SPASS

cmps_PONTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PONTPPi", "TPP_def", "ga_non_empty_sort_Reg",
                     "?_RCC5", "?_RCC8", "P_impl_O", "EQ_def", "PPi_def", "PO_def",
                     "PP_def", "sym_PO", "NTPPi_def", "TPPi_def", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "disj_PP", "disj_EC", "disj_NTPP",
                     "disj_NTPPi", "DR_eq_DC_or_EC", "cmps_ECNTPPi", "cmps_PP",
                     "P_inh_O", "cmps_PPiPO", "?_RCC5_def", "?_RCC8_def"
        Prover: SPASS

cmps_TPPDC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPDC", "DC_def", "C_sym", "P_impl_O", "PP_def",
                     "PP_eq_TPP_or_NTPP", "sym_DC", "disj_TPP", "PO_def", "P_def",
                     "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_TPPEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPEC", "sym_DR", "DR_eq_DC_or_EC",
                     "PP_eq_TPP_or_NTPP", "sym_EC", "cmps_PPDR"
        Prover: SPASS

cmps_TPPPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPPO", "?_RCC5", "PPi_def", "PP_def", "sym_PO",
                     "sym_DR", "TPPi_def", "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi",
                     "PO_def", "DR_eq_DC_or_EC", "cmps_PPPP", "cmps_EQPP", "?_RCC5_def"
        Prover: SPASS

cmps_TPPTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPTPP", "PP_eq_TPP_or_NTPP", "cmps_PPPP"
        Prover: SPASS

cmps_TPPNTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPNTPP", "TPP_def", "ga_non_empty_sort_Reg",
                     "DC_def", "P_impl_O", "O_sym", "PPi_def", "PP_def", "sym_EC",
                     "sym_DC", "NTPPi_def", "TPPi_def", "NTPP_def", "P_def",
                     "ga_non_empty_sort_QReg", "PO_def", "disj_PP", "disj_PO",
                     "disj_TPPi", "disj_NTPP", "disj_TPP", "disj_EC", "disj_DC",
                     "PPi_eq_TPPi_or_NTPPi", "PP_eq_TPP_or_NTPP", "cmps_ECNTPPi",
                     "cmps_TPPDC", "cmps_PPPP", "P_inh_O", "cmps_ECNTPP", "cmps_POTPP",
                     "cmps_PONTPP"
        Prover: SPASS

cmps_TPPTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPTPPi", "?_RCC5", "EQ_def", "PPi_def",
                     "sym_PO", "sym_DR", "NTPPi_def", "TPPi_def", "disj_TPPi",
                     "disj_TPP", "PPi_eq_TPPi_or_NTPPi", "DR_eq_DC_or_EC",
                     "cmps_TPPiNTPPi", "?_RCC5_def"
        Prover: SPASS

cmps_TPPNTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPNTPPi", "?_RCC5", "P_impl_O", "EQ_def",
                     "PPi_def", "PP_def", "PPi_eq_TPPi_or_NTPPi", "NTPPi_def", "DR_def",
                     "disj_PP", "disj_NTPP", "disj_TPP", "PP_eq_TPP_or_NTPP",
                     "DR_eq_DC_or_EC", "cmps_TPPNTPP", "cmps_NTPPNTPP",
                     "cmps_TPPiNTPPi", "?_RCC5_def"
        Prover: SPASS

cmps_NTPPDC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPDC", "DC_def", "C_sym", "PP_def",
                     "PP_eq_TPP_or_NTPP", "sym_DC", "P_def", "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_NTPPEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPEC", "EQ_def", "PPi_def", "sym_EQ",
                     "sym_DR", "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "sym_EC", "disj_DR", "disj_EC",
                     "cmps_PPDR", "cmps_TPPEC", "cmps_ECNTPP"
        Prover: SPASS

cmps_NTPPPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPPO", "?_RCC5", "P_impl_O", "O_sym",
                     "EQ_def", "PPi_def", "PO_def", "PP_def", "sym_PO", "sym_DR",
                     "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "sym_EC", "P_def",
                     "ga_non_empty_sort_QReg", "disj_NTPP", "cmps_PP", "P_inh_O",
                     "?_RCC5_def"
        Prover: SPASS

cmps_NTPPTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPTPP", "?_RCC5", "DC_def", "P_impl_O",
                     "PPi_def", "PP_def", "sym_PO", "PPi_eq_TPPi_or_NTPPi", "TPPi_def",
                     "NTPP_def", "ga_non_empty_sort_Reg", "TPP_def", "disj_PP",
                     "disj_PO", "disj_TPP", "disj_EC", "disj_DC", "PP_eq_TPP_or_NTPP",
                     "DR_eq_DC_or_EC", "PO_def", "cmps_TPPNTPP", "cmps_NTPPNTPP",
                     "cmps_PPPP", "P_def", "ga_non_empty_sort_QReg", "?_RCC5_def",
                     "cmps_TPPiNTPP"
        Prover: SPASS

cmps_NTPPNTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPNTPP", "TPP_def", "ga_non_empty_sort_Reg",
                     "?_RCC5", "DC_def", "C_non_null", "P_impl_O", "O_sym", "PPi_def",
                     "PP_def", "NTPPi_def", "TPPi_def", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "sym_DC", "sym_EC", "DR_def", "PO_def",
                     "disj_PO", "disj_EC", "disj_TPP", "disj_NTPP", "disj_NTPPi",
                     "cmps_NTPPDC", "cmps_ECNTPPi", "cmps_PPPP", "cmps_PP", "NTP_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def", "cmps_ECNTPP"
        Prover: SPASS

cmps_NTPPTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPTPPi", "?_RCC5", "EQ_def", "NTPPi_def",
                     "TPPi_def", "disj_TPP", "PPi_eq_TPPi_or_NTPPi",
                     "PP_eq_TPP_or_NTPP", "DR_eq_DC_or_EC", "cmps_TPPNTPP",
                     "cmps_NTPPNTPP", "?_RCC5_def"
        Prover: SPASS

cmps_NTPPNTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPNTPPi", "?_RCC8"
        Prover: SPASS

cmps_TPPiDC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiDC", "?_RCC5", "DC_def", "C_sym",
                     "C_non_null", "EQ_def", "PPi_def", "PP_def",
                     "PPi_eq_TPPi_or_NTPPi", "disj_TPPi", "DR_eq_DC_or_EC",
                     "cmps_EQPPi", "P_def", "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_TPPiEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiEC", "?_RCC5", "DC_def", "C_sym", "PPi_def",
                     "PP_def", "EC_def", "DR_eq_DC_or_EC", "PPi_eq_TPPi_or_NTPPi",
                     "sym_DC", "sym_EC", "disj_DR", "cmps_PPDR", "cmps_EQDR", "P_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_TPPiPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiPO", "?_RCC5", "PPi_def", "PO_def",
                     "PP_def", "sym_PO", "PPi_eq_TPPi_or_NTPPi", "DR_def", "disj_PO",
                     "disj_TPPi", "cmps_PPPP", "cmps_EQPO", "P_inh_O", "?_RCC5_def"
        Prover: SPASS

cmps_TPPiTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiTPP", "?_RCC5", "P_impl_O", "PPi_def",
                     "PP_def", "PPi_eq_TPPi_or_NTPPi", "NTPPi_def", "TPPi_def",
                     "TPP_def", "ga_non_empty_sort_Reg", "DR_def", "disj_TPPi",
                     "PP_eq_TPP_or_NTPP", "cmps_TPPNTPP", "cmps_NTPPiTPPi", "P_inh_O",
                     "?_RCC5_def"
        Prover: SPASS

cmps_TPPiNTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiNTPP", "TPP_def", "ga_non_empty_sort_Reg",
                     "?_RCC5", "DC_def", "P_impl_O", "O_sym", "EQ_def", "PPi_def",
                     "PP_def", "sym_PO", "PPi_eq_TPPi_or_NTPPi", "DR_eq_DC_or_EC",
                     "NTPPi_def", "TPPi_def", "NTPP_def", "P_def",
                     "ga_non_empty_sort_QReg", "DR_def", "PO_def", "disj_PP", "disj_PO",
                     "disj_DR", "disj_NTPPi", "disj_TPPi", "disj_NTPP", "disj_TPP",
                     "disj_EC", "PP_eq_TPP_or_NTPP", "cmps_TPPNTPP", "cmps_TPPiNTPPi",
                     "cmps_NTPPiNTPPi", "cmps_PPPP", "cmps_PP", "P_inh_O", "NTP_def",
                     "?_RCC5_def", "cmps_ECNTPP", "cmps_PONTPP"
        Prover: SPASS

cmps_TPPiTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiTPPi", "PPi_def", "TPPi_def",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "cmps_PPPP"
        Prover: SPASS

cmps_TPPiNTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_TPPiNTPPi", "TPP_def", "ga_non_empty_sort_Reg",
                     "P_impl_O", "PPi_def", "PP_def", "NTPPi_def", "DR_eq_DC_or_EC",
                     "PP_eq_TPP_or_NTPP", "PPi_eq_TPPi_or_NTPPi", "P_def",
                     "ga_non_empty_sort_QReg", "PO_def", "disj_EC", "cmps_ECNTPPi",
                     "cmps_DCNTPPi", "cmps_PPPP", "cmps_DRPPi", "P_inh_O"
        Prover: SPASS

cmps_NTPPiDC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiDC", "?_RCC5", "DC_def", "C_sym",
                     "C_non_null", "EQ_def", "PPi_def", "PP_def",
                     "PPi_eq_TPPi_or_NTPPi", "disj_NTPPi", "DR_eq_DC_or_EC", "P_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_NTPPiEC
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiEC", "?_RCC5", "DC_def", "C_sym", "PP_def",
                     "NTPPi_def", "EC_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "sym_DC", "sym_EC", "disj_EC", "disj_NTPPi",
                     "PPi_eq_TPPi_or_NTPPi", "cmps_TPPiNTPPi", "cmps_ECNTPPi",
                     "cmps_PPDR", "cmps_EQDR", "P_def", "ga_non_empty_sort_QReg",
                     "?_RCC5_def"
        Prover: SPASS

cmps_NTPPiPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiPO", "?_RCC5", "O_impl_C", "O_sym",
                     "EQ_def", "PO_def", "PP_def", "sym_PO", "sym_DR", "NTPPi_def",
                     "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP", "DR_def",
                     "DC_def", "disj_NTPPi", "PPi_eq_TPPi_or_NTPPi", "cmps_TPPiNTPPi",
                     "cmps_NTPPNTPP", "cmps_ECNTPPi", "P_def", "ga_non_empty_sort_QReg",
                     "?_RCC5_def"
        Prover: SPASS

cmps_NTPPiTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiTPP", "?_RCC5", "EQ_def", "PPi_def",
                     "sym_PO", "sym_DR", "NTPPi_def", "TPPi_def",
                     "PPi_eq_TPPi_or_NTPPi", "disj_NTPP", "disj_NTPPi",
                     "DR_eq_DC_or_EC", "cmps_TPPiNTPPi", "cmps_NTPPNTPP", "cmps_DRPPi",
                     "?_RCC5_def"
        Prover: SPASS

cmps_NTPPiNTPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiNTPP", "?_RCC5", "P_impl_O", "O_sym",
                     "PP_def", "sym_DR", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "DR_def", "PPi_eq_TPPi_or_NTPPi", "cmps_ECNTPPi", "cmps_DCNTPPi",
                     "?_RCC5_def"
        Prover: SPASS

cmps_NTPPiTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiTPPi", "TPP_def", "ga_non_empty_sort_Reg",
                     "?_RCC5", "O_impl_C", "P_impl_O", "EQ_def", "PO_def", "PP_def",
                     "NTPPi_def", "TPPi_def", "DR_eq_DC_or_EC", "PP_eq_TPP_or_NTPP",
                     "PPi_eq_TPPi_or_NTPPi", "DR_def", "disj_PP", "DC_def", "disj_EC",
                     "disj_TPP", "disj_NTPP", "disj_NTPPi", "cmps_TPPiNTPPi",
                     "cmps_ECNTPPi", "cmps_DCTPPi", "cmps_PP", "P_inh_O", "P_def",
                     "ga_non_empty_sort_QReg", "?_RCC5_def"
        Prover: SPASS

cmps_NTPPiNTPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_NTPPiNTPPi", "NTPPi_def", "cmps_NTPPNTPP"
        Prover: SPASS