?_RCC5
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "?_RCC5", "C_id", "ga_non_empty_sort_QReg", "DR_def",
                     "O_impl_C", "O_sym", "?_RCC5_def", "EQ_def", "PPi_def", "PP_def",
                     "PO_def", "P_def", "NTP_def"
        Prover: SPASS

sym_DR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "sym_DR", "DR_def", "O_sym"
        Prover: SPASS

sym_PO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "sym_PO", "O_sym", "PO_def"
        Prover: SPASS

sym_EQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "sym_EQ", "EQ_def"
        Prover: SPASS

disj_DR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_DR", "P_impl_O", "O_sym", "EQ_def", "PPi_def",
                     "PO_def", "PP_def", "sym_DR", "sym_PO", "P_def",
                     "ga_non_empty_sort_QReg", "DR_def"
        Prover: SPASS

disj_PO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_PO", "EQ_def", "PPi_def", "PP_def", "sym_DR",
                     "sym_PO", "P_def", "ga_non_empty_sort_QReg", "PO_def", "disj_DR"
        Prover: SPASS

disj_PP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_PP", "P_impl_O", "O_sym", "EQ_def", "PPi_def",
                     "PP_def", "sym_DR", "DR_def", "disj_PO"
        Prover: SPASS

disj_PPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_PPi", "P_impl_O", "EQ_def", "PPi_def", "PP_def",
                     "sym_DR", "sym_PO", "DR_def", "disj_PP"
        Prover: SPASS

disj_EQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "disj_EQ", "EQ_def", "PPi_def", "sym_EQ", "disj_DR",
                     "disj_PO", "disj_PPi"
        Prover: SPASS

cmps_PPPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPPP", "P_impl_O", "O_sym", "PPi_def", "PP_def",
                     "disj_PPi", "PO_def", "cmps_PP", "P_inh_O"
        Prover: SPASS

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

cmps_PPPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPPO", "DR_def", "C_non_null", "O_impl_C",
                     "P_impl_O", "O_sym", "PPi_def", "PP_def", "sym_PO", "PO_def",
                     "disj_PPi", "cmps_PP", "NTP_def", "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_PPDR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPDR", "DR_def", "P_impl_O", "O_sym", "PPi_def",
                     "PO_def", "PP_def", "sym_DR", "sym_PO", "disj_PP", "disj_PPi",
                     "cmps_PPPP", "P_inh_O"
        Prover: SPASS

cmps_PPEQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPEQ", "EQ_def", "sym_EQ"
        Prover: SPASS

cmps_PPiPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPiPP", "P_impl_O", "PPi_def", "PP_def",
                     "DR_def", "disj_PP", "PO_def", "P_inh_O"
        Prover: SPASS

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

cmps_PPiPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPiPO", "?_RCC5", "P_impl_O", "O_sym", "EQ_def",
                     "PPi_def", "PO_def", "PP_def", "sym_PO", "DR_def", "disj_PP",
                     "cmps_PPPP", "P_inh_O", "?_RCC5_def"
        Prover: SPASS

cmps_PPiDR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPiDR", "DR_def", "C_sym", "O_impl_C",
                     "P_impl_O", "O_sym", "PPi_def", "PP_def", "sym_DR", "sym_PO",
                     "disj_PPi", "PO_def", "P_inh_O", "P_def", "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_PPiEQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPiEQ", "EQ_def", "sym_EQ"
        Prover: SPASS

cmps_POPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POPP", "P_impl_O", "O_sym", "PPi_def", "PO_def",
                     "PP_def", "P_def", "ga_non_empty_sort_QReg", "DR_def", "disj_PPi",
                     "cmps_PP", "P_inh_O", "cmps_PPPO"
        Prover: SPASS

cmps_POPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POPPi", "?_RCC5", "P_impl_O", "EQ_def",
                     "PPi_def", "PP_def", "disj_PP", "disj_PPi", "PO_def", "cmps_PPiPO",
                     "?_RCC5_def"
        Prover: SPASS

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

cmps_PODR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PODR", "DR_def", "O_impl_C", "O_sym", "PPi_def",
                     "PO_def", "sym_DR", "sym_PO", "PP_def", "P_inh_O", "P_def",
                     "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_POEQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POEQ", "EQ_def", "sym_EQ"
        Prover: SPASS

cmps_DRPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DRPP", "DR_def", "O_impl_C", "P_impl_O",
                     "O_sym", "PP_def", "sym_PO", "PO_def", "P_inh_O", "NTP_def",
                     "ga_non_empty_sort_QReg"
        Prover: SPASS

cmps_DRPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DRPPi", "PPi_def", "sym_DR", "cmps_PPDR"
        Prover: SPASS

cmps_DRPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DRPO", "DR_def", "C_non_null", "O_impl_C",
                     "O_sym", "PO_def", "sym_PO", "PP_def", "P_inh_O", "NTP_def",
                     "ga_non_empty_sort_QReg"
        Prover: SPASS

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

cmps_DREQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DREQ", "EQ_def", "sym_EQ"
        Prover: SPASS

cmps_EQPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_EQPP", "EQ_def"
        Prover: SPASS

cmps_EQPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_EQPPi", "EQ_def"
        Prover: SPASS

cmps_EQPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_EQPO", "EQ_def"
        Prover: SPASS

cmps_EQDR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_EQDR", "EQ_def"
        Prover: SPASS

cmps_EQEQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_EQEQ", "EQ_def", "sym_EQ"
        Prover: SPASS