OWL 2 Full Example "Mutual Love" (TPTP)

% This is the translation of the example for mutual love
% based on a functional "loves" relation into TPTP.
% "conclusion.tptp" and "premise.tptp" are the
% conclusion and premise, respectively, translated
% from the respective RDF files at
% <http://pastebin.com/W8n6YuQN>.
% owl2full_sufficientaxioms.tptp is the translation
% of a small fragment of the full set of
% OWL 2 RDF-Based semantic conditions into TPTP,
% which is sufficient to prove the result.
% To do OWL 2 Full reasoning, just copy and paste
% this whole file into any TPTP-aware FOL theorem prover.
% There are plenty of FOL reasoners at
%     <http://tptp.org/cgi-bin/SystemOnTPTP>

% ============= conclusion.tptp ==================

fof(conclusion,conjecture,(
    iext(uri_ex_mutuallyLoves,uri_ex_Naoko,uri_ex_Sato) )).

% ============= premise.tptp =====================

fof(premise,axiom,(
    ? [X1,X2,X0,X3] :
      ( iext(uri_ex_loves,uri_ex_Sato,uri_ex_Naoko)
      & iext(uri_rdfs_subPropertyOf,uri_ex_mutuallyLoves,uri_ex_loves)
      & iext(uri_owl_inverseOf,uri_ex_lovedBy,uri_ex_loves)
      & iext(uri_owl_minCardinality,X0,literal_typed(dat_str_1,uri_xsd_nonNegativeInteger))
      & iext(uri_owl_onProperty,X0,uri_ex_mutuallyLoves)
      & iext(uri_rdf_type,X0,uri_owl_Restriction)
      & iext(uri_ex_loves,uri_ex_Naoko,uri_ex_Sato)
      & iext(uri_owl_equivalentClass,uri_ex_MutuallyLoved,X0)
      & iext(uri_owl_equivalentClass,uri_ex_MutuallyLoved,X1)
      & iext(uri_owl_hasSelf,X1,literal_typed(dat_str_true,uri_xsd_boolean))
      & iext(uri_owl_onProperty,X1,uri_ex_lovesLovedBy)
      & iext(uri_owl_propertyChainAxiom,uri_ex_lovesLovedBy,X2)
      & iext(uri_rdf_rest,X3,uri_rdf_nil)
      & iext(uri_rdf_first,X3,uri_ex_lovedBy)
      & iext(uri_rdf_type,uri_ex_loves,uri_owl_FunctionalProperty)
      & iext(uri_rdf_rest,X2,X3)
      & iext(uri_rdf_first,X2,uri_ex_loves) ) )).

% ============= owl2full_sufficientaxioms.tptp ===

fof(simple_ir, axiom, (
    ! [X] : (
        ir(X) ))) .

fof(rdfs_ic_def, axiom, (
    ! [X] : (
            ic(X)
        <=>
            icext(uri_rdfs_Class, X) ))) .

fof(rdfs_cext_def, axiom, (
    ! [X, C] : (
            iext(uri_rdf_type, X, C)
        <=>
            icext(C, X) ))) .

fof(owl_chain_002, axiom, (
    ! [P, S1, P1, S2, P2] : (
            ( iext(uri_rdf_first, S1, P1)
            & iext(uri_rdf_rest, S1, S2)
            & iext(uri_rdf_first, S2, P2)
            & iext(uri_rdf_rest, S2, uri_rdf_nil) )
        => (
               iext(uri_owl_propertyChainAxiom, P, S1)
           <=> (
                 ip(P)
               & ip(P1)
               & ip(P2)
               & ( ! [Y0, Y1, Y2] : (
                       ( iext(P1, Y0, Y1)
                       & iext(P2, Y1, Y2) )
                   =>
                       iext(P, Y0, Y2) ))))))) .

fof(owl_inv, axiom, (
    ! [P1, P2] : (
            iext(uri_owl_inverseOf, P1, P2)
        <=> (
              ip(P1)
            & ip(P2)
            & ( ! [X, Y] : (
                    iext(P1, X, Y)
                <=>
                    iext(P2, Y, X) )))))) .

fof(owl_eqdis_equivalentclass, axiom, (
    ! [C1, C2] : (
            iext(uri_owl_equivalentClass, C1, C2)
        <=> (
              ic(C1)
            & ic(C2)
            & ( ! [X] : (
                    icext(C1, X)
                <=>
                    icext(C2, X) )))))) .

fof(owl_rdfsext_subpropertyof, axiom, (
    ! [P1, P2] : (
            iext(uri_rdfs_subPropertyOf, P1, P2)
        <=> (
              ip(P1)
            & ip(P2)
            & ( ! [X, Y] : (
                    iext(P1, X, Y)
                =>
                    iext(P2, X, Y) )))))) .


fof(owl_char_functional, axiom, (
    ! [P] : (
            icext(uri_owl_FunctionalProperty, P)
        <=> (
              ip(P)
            & ( ! [X, Y1, Y2] : (
                    ( iext(P, X, Y1)
                    & iext(P, X, Y2) )
                =>
                    Y1 = Y2 )))))) .

fof(owl_restrict_mincard_001, axiom, (
    ! [Z, P] : (
           ( iext(uri_owl_minCardinality, Z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger))
           & iext(uri_owl_onProperty, Z, P) )
        => (
            ! [X] : (
                    icext(Z, X)
                <=> (
                      ? [Y] :
                          iext(P, X, Y) )))))) .

fof(owl_restrict_hasself, axiom, (
    ! [Z, P, V] : (
            ( iext(uri_owl_hasSelf, Z, V)
            & iext(uri_owl_onProperty, Z, P) )
        => (
            ! [X] : (
                    icext(Z, X)
                <=>
                    iext(P, X, X) ))))) .