# Generated with http://www.agfa.com/w3c/euler/#R3680 on 20 Dec 2003 15:51:36 GMT
{
 (
 <http://www.agfa.com/w3c/euler/graph.axiom.n3>.<http://www.w3.org/2000/10/swap/log#semantics>
 <http://www.agfa.com/w3c/euler/owl-rules.n3>.<http://www.w3.org/2000/10/swap/log#semantics>
 <http://www.agfa.com/w3c/euler/rdfs-rules.n3>.<http://www.w3.org/2000/10/swap/log#semantics>
 ).<http://www.w3.org/2000/10/swap/log#conjunction> =>
 <http://www.agfa.com/w3c/euler/graph.lemma.n3>.<http://www.w3.org/2000/10/swap/log#semantics>
}
<http://www.w3.org/2000/10/swap/reason#because>
{
@prefix str: <http://www.w3.org/2000/10/swap/string#>.
@prefix ns0: <http://www.agfa.com/w3c/euler/owl-rules#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix : <http://www.agfa.com/w3c/euler/graph.axiom#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix ns1: <http://www.agfa.com/w3c/euler/rdfs-rules#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix iw: <http://www.ksl.stanford.edu/software/IW/spec/iw#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

 {
  ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
  :route rdf:type owl:TransitiveProperty. 
   {
    ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
    [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
     {
      ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
      [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
      [iw:Variable "?S"; = :angers] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :nantes]} =>
    {[iw:Variable "?S"; = :angers] :twoway [iw:Variable "?O"; = :nantes]}} =>
  {[iw:Variable "?X"; = :angers] :route [iw:Variable "?O"; = :nantes]}. 
   {
    ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
    :route rdf:type owl:TransitiveProperty. 
     {
      ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
      [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
       {
        ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
        [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
        [iw:Variable "?S"; = :lemans] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :angers]} =>
      {[iw:Variable "?S"; = :lemans] :twoway [iw:Variable "?O"; = :angers]}} =>
    {[iw:Variable "?X"; = :lemans] :route [iw:Variable "?O"; = :angers]}. 
     {
      ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
      :route rdf:type owl:TransitiveProperty. 
       {
        ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
        [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
         {
          ns0:owl1s1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
          :twoway rdf:type owl:SymmetricProperty. 
           {
            ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
            [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
            [iw:Variable "?S"; = :lemans] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :tours]} =>
          {[iw:Variable "?S"; = :lemans] :twoway [iw:Variable "?O"; = :tours]}} =>
        {[iw:Variable "?S"; = :tours] :twoway [iw:Variable "?O"; = :lemans]}} =>
      {[iw:Variable "?X"; = :tours] :route [iw:Variable "?O"; = :lemans]}. 
       {
        ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
        :route rdf:type owl:TransitiveProperty. 
         {
          ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
          [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
           {
            ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
            [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
            [iw:Variable "?S"; = :blois] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :tours]} =>
          {[iw:Variable "?S"; = :blois] :twoway [iw:Variable "?O"; = :tours]}} =>
        {[iw:Variable "?X"; = :blois] :route [iw:Variable "?O"; = :tours]}. 
         {
          ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
          :route rdf:type owl:TransitiveProperty. 
           {
            ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
            [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
             {
              ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
              [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
              [iw:Variable "?S"; = :orleans] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :blois]} =>
            {[iw:Variable "?S"; = :orleans] :twoway [iw:Variable "?O"; = :blois]}} =>
          {[iw:Variable "?X"; = :orleans] :route [iw:Variable "?O"; = :blois]}. 
           {
            ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
            :route rdf:type owl:TransitiveProperty. 
             {
              ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
              [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
               {
                ns0:owl1s1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
                :twoway rdf:type owl:SymmetricProperty. 
                 {
                  ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
                  [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
                  [iw:Variable "?S"; = :orleans] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :bourges]} =>
                {[iw:Variable "?S"; = :orleans] :twoway [iw:Variable "?O"; = :bourges]}} =>
              {[iw:Variable "?S"; = :bourges] :twoway [iw:Variable "?O"; = :orleans]}} =>
            {[iw:Variable "?X"; = :bourges] :route [iw:Variable "?O"; = :orleans]}. 
             {
              ns0:owl2t1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
              :route rdf:type owl:TransitiveProperty. 
               {
                ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
                [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
                 {
                  ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
                  [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
                  [iw:Variable "?S"; = :orleans] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :bourges]} =>
                {[iw:Variable "?S"; = :orleans] :twoway [iw:Variable "?O"; = :bourges]}} =>
              {[iw:Variable "?X"; = :orleans] :route [iw:Variable "?O"; = :bourges]}. 
               {
                ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
                [iw:Variable "?P"; = :twoway] rdfs:subPropertyOf :route. 
                 {
                  ns0:owl1s1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
                  :twoway rdf:type owl:SymmetricProperty. 
                   {
                    ns0:owl1s1 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/owl-rules>]. 
                    :twoway rdf:type owl:SymmetricProperty. 
                     {
                      ns1:rdfs7 log:racine [iw:Variable "?LR"; = <http://www.agfa.com/w3c/euler/rdfs-rules>]. 
                      [iw:Variable "?P"; = :oneway] rdfs:subPropertyOf :twoway. 
                      [iw:Variable "?S"; = :parijs] [iw:Variable "?P"; = :oneway] [iw:Variable "?O"; = :orleans]} =>
                    {[iw:Variable "?S"; = :parijs] :twoway [iw:Variable "?O"; = :orleans]}} =>
                  {[iw:Variable "?S"; = :orleans] :twoway [iw:Variable "?O"; = :parijs]}} =>
                {[iw:Variable "?S"; = :parijs] :twoway [iw:Variable "?O"; = :orleans]}} =>
              {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :orleans]}} =>
            {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :bourges]}} =>
          {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :orleans]}} =>
        {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :blois]}} =>
      {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :tours]}} =>
    {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :lemans]}} =>
  {[iw:Variable "?S"; = :parijs] :route [iw:Variable "?X"; = :angers]}} =>
{:parijs :route :nantes}. 
<http://www.agfa.com/w3c/euler/graph.axiom#parijs> <http://www.w3.org/2002/07/owl#sameAs> <http://www.agfa.com/w3c/euler/graph.axiom#paris>.
<http://www.agfa.com/w3c/euler/graph.axiom#path> <http://www.w3.org/2002/07/owl#sameAs> <http://www.agfa.com/w3c/euler/graph.axiom#route>.
# Proof found for http://www.agfa.com/w3c/euler/graph.lemma.n3 in 2614 steps (5434 steps/sec) using 1 engine
}.