triv
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "triv", "C_id", "ga_non_empty_sort_QReg", "DR_def",
                     "O_sym", "?_def", "EQ_def", "PPi_def", "PP_def", "PO_def", "P_def"
        Prover: SPASS

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

cmps_PPPPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPPPi", "triv"
        Prover: SPASS

cmps_PPPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPPO", "Ax1", "DR_def", "C_non_null",
                     "P_impl_O", "O_sym", "PO_def", "PP_def", "cmps_PP", "P_def", "Ax8",
                     "NTP_def"
        Prover: SPASS

cmps_PPDR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open

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

cmps_PPiPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPiPP", "Ax1", "C_non_null", "P_impl_O",
                     "O_sym", "PPi_def", "PP_def", "DR_def", "PO_def", "P_def", "Ax8",
                     "O_def"
        Prover: SPASS

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

cmps_PPiPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open

cmps_PPiDR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_PPiDR", "Ax1", "DR_def", "P_impl_O", "O_sym",
                     "PPi_def", "PO_def", "PP_def", "cmps_PP", "P_def", "Ax8"
        Prover: SPASS

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

cmps_POPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open

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

cmps_POPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_POPO", "triv"
        Prover: SPASS

cmps_PODR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open

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

cmps_DRPP
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DRPP", "DR_def", "P_impl_O", "O_sym", "PPi_def",
                     "PP_def", "P_def", "Ax8", "PO_def", "cmps_PPiPPi", "?_def",
                     "cmps_PPiDR"
        Prover: SPASS

cmps_DRPi
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open

cmps_DRPO
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open

cmps_DRDR
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Open
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DRDR", "triv"
        Prover: SPASS

cmps_DREQ
    Com: CASL2SPASS : CASL -> SPASS
        Status: Proved
        Used axioms: "cmps_DREQ", "EQ_def"
        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"
        Prover: SPASS