\chapter{Example Notation3 Files}
\section{TREAT Example}
Some Notation3 rules performance problems can be more easily solved than they ones in Appendix \ref{turing} or Appendix \ref{evil-n3}. As an example, we have \uri{http://www.w3.org/2000/10/swap/test/reason/longChain.n3}

\uri{http://www.w3.org/2000/10/swap/test/reason/shortChain.n3} is a somewhat shorter version of the same thing, which is reproduced below. 
\label{loopy-n3}
\begin{verbatim}
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>. 
 :foo a :Class1 . 
 {?x a ?C1 . ?C1 rdfs:subClassOf ?C2} => {?x a ?C2} . 
 :Class1 rdfs:subClassOf :Class2 .
:Class2 rdfs:subClassOf :Class3 .
:Class3 rdfs:subClassOf :Class4 .
:Class4 rdfs:subClassOf :Class5 .
:Class5 rdfs:subClassOf :Class6 .
:Class6 rdfs:subClassOf :Class7 .
:Class7 rdfs:subClassOf :Class8 .
:Class8 rdfs:subClassOf :Class9 .
:Class9 rdfs:subClassOf :Class10 .
:Class10 rdfs:subClassOf :Class11 .
\end{verbatim}

\section{Inconsistent RDFS}
\label{inconsistentrdfs}
It is possible for a RDFS file to be inconsistent. The example given in the standard follows.
\begin{verbatim}
<ex:a> <ex:p> "<notLegalXML"^^rdf:XMLLiteral .
<ex:p> rdfs:range rdf:XMLLiteral . 
\end{verbatim}

\section{Turing Completeness of Notation3 Rules}
\label{turing}
Because Notation3 does not have functions, it is not trivial that Notation3 rules are universal. Nonetheless, any implementation that allows for implying existentials, in the pattern of
\begin{verbatim}
{...} => {@forSome :A . ... } .
\end{verbatim}
should still be universal. Included here is a file \uri{http://www.w3.org/2000/10/swap/turing/unlambda.n3}, which is an implementation of the $s$ and $k$ combinators in Notation3 rules. If one accepts that this file is valid and runs, then Notation3 rules can emulate $s$ and $k$ combinators. The file is a simple eval/apply loop, based directly on \cite{sicp}

\begin{verbatim}
@prefix : <http://yosi.us/unlambda#> .
#@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@keywords a, of, is .
#
# An combinators interpreter.n3
# usage: cwm un_expr.n3 --think=unlambda.n3 --filter=un_filter.n3
# see un_expr.n3 for examples

#
# Begin defining what needs to be eval'ed
{?x a RootExpression} => {?x a NeedsEval} .

#recursive step of eval #1
{(?x ?y) a NeedsEval}
=>
{?x a NeedsEval .
 ?y a NeedsEval} .

#{?x a NeedsEval; log:rawType log:Other} => {?x eval ?x} .
#base case of eval
{k a NeedsEval} => {k eval k} .
{s a NeedsEval} => {s eval s} .
{v a NeedsEval} => {v eval v} .
{i a NeedsEval} => {i eval i} .

#
# Eval calls apply
{ (?x ?y) a NeedsEval .
 ?x eval ?a .
 ?y eval ?b .
}
=>
{(?a ?b) a NeedsApply} .

#
#Eval gets the return value from apply, and returns it
{(?x ?y) a NeedsEval .
 ?x eval ?a .
 ?y eval ?b .
 (?a ?b) apply ?c . }
=>
{(?x ?y) eval ?c } .

#
#apply (k x)
{(k ?x) apply (k ?x)}
<=
{(k ?x) a NeedsApply} .


#apply ((k y) x) ==> y
#
{((k ?y) ?x) apply ?y}
<=
{((k ?y) ?x) a NeedsApply} .

# apply (s x)
#
{(s ?x) apply (s ?x)}
<=
{(s ?x) a NeedsApply} .

# apply ((s y) x)
#
{((s ?y) ?x) apply ((s ?y) ?x)}
<=
{((s ?y) ?x) a NeedsApply } .

# apply (((s z) y) x)
# calls (z x) and (y x)
{(((s ?y) ?z) ?x) a NeedsApply .
} =>
{(?y ?x) a NeedsEval .
 (?z ?x) a NeedsEval } .

# apply (((s z) y) x)
# gets (z x) and (y x)
# and calls ((z x) (y x))
{(((s ?y) ?z) ?x) a NeedsApply .
 (?y ?x) eval ?r .
 (?z ?x) eval ?s .
}
=>
{(?r ?s) a NeedsEval} .
# apply (((s z) y) x)
# gets ((z x) (y x))
# and returns it
{(((s ?y) ?z) ?x) a NeedsApply .
 (?y ?x) eval ?r .
 (?z ?x) eval ?s .
 (?r ?s) eval ?w }
=>
{(((s ?y) ?z) ?x) apply ?w} .

# (i x) ==> x
#
{(i ?x) apply ?x}
<=
{(i ?x) a NeedsApply} .

# (v x) ==> v
#
{(v ?x) apply v}
<=
{(v ?x) a NeedsApply} .
\end{verbatim}

\chapter{Avoiding Redundant Rule Firings}
\label{skolem-vs-entailment}
Cwm tries to insure that it does not redundantly fire rules by treating existentials as skolem functions, functions of all variables bound that appear in the conclusion. Let us see an example.
\begin{verbatim}
{?X @has :uncle ?Y}
=>
{@forSome :A . ?A @has :brother ?Y} .
\end{verbatim}
This rules says that an uncle is somebody's brother. We note that $?Y$ appears in the conclusion, but $?X$ does not. This does matter. If two people both have $?Y$ as an uncle, we still only know that $?Y$ is somebody's brother. If $X$ has two uncles, they may very well not be brothers of the same person, we cannot assert \verb|[:brother :Q1, :Q2]|. By making the existential a function of $Y$, we get the effect we want, at the cost of a hash table lookup.

This can still lead to the creation of redundant statements. The rule we already looked at
\begin{verbatim}
{?X a :Man} => {[a :Man]} .
\end{verbatim}
should never fire. What it generates is redundant. Nonetheless, Cwm will generate a single \verb|[a :Man]| triple by these rules, though it will not generate any others. In a conversation, Chris Hanson mentioned that if instead Cwm tested if the new triples were entailed by the existing graph, given that all anonymous nodes that appear in the graph are treated as unique individuals instead of the usual treatment of blank nodes, then this would be a complete test to insure rules generate only exactly what is needed. This would involve doing a second search after the pattern in the rules already matched --- a much more expensive operation. Therefore, Cwm does not do this anymore.

\chapter{Notation3 Rules are still Computationally Intractable}
\label{evil-n3}
The following Notation3 rule appears nowhere in any file in the wild. This is certainly because people are interested in computing useful things, and not simply making rule engines work.
\begin{verbatim}
{?X1 ?X2 ?X3 .
 ?Y1 ?Y2 ?Y3 .
 ?Z1 ?Z2 ?Z3 } => {?X2 ?Y3 ?Z1} .
\end{verbatim}

This rule does not imply an existential, so it must terminate. That said, it has a number of bad properties.
\begin{itemize}
\item It matches against every statement in the system three times. This means that the number of matches generated is the cube of the current number of statements
\item It generates a maximal graph. Given $n$ RDF terms, there are $n^3$ possible statements it can generate. This rule will not stop until it generates them all.
\end{itemize}


\chapter{An example AIR file}
\label{arl2-scenario}
What follows is the file \url{http://dig.csail.mit.edu/2008/ARL/udhr-policy.n3}. This is a simple AIR file.
\begin{verbatim}
# ARL scenario, violation of Universal Declaration of Human rights, Article 12
# http://www.unhchr.ch/udhr/lang/eng.htm

# more about ARL scenario http://dig.csail.mit.edu/2008/ARL

# $Date: 2008-02-29 18:02:15 -0500 (Fri, 29 Feb 2008) $
# $Revision: 15842 $
# $Author: lkagal $

@prefix rdf:  <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix foaf: <http://xmlns.com/foaf/0.1/> .
@prefix owl:  <http://www.w3.org/2002/07/owl#> .

@prefix air: <http://dig.csail.mit.edu/TAMI/2007/amord/air#> .	
@prefix tami: <http://dig.csail.mit.edu/TAMI/2007/tami#> .

@prefix :  <http://dig.csail.mit.edu/2008/ARL/policy#> .	

:Universal_Declaration_of_Human_Rights_Article12 a air:Policy;
	rdfs:label "Universal Declaration of Human Rights, Article 12";
	rdfs:comment "Under the Universal Declaration of Human Rights no one should be subjected to arbitrary interference with respect to privacy and home. Any search carried out without due process i.e. without giving notice or obtaining consent, violates this.";
	air:variable :COMPLAINT, :SEARCHEVENT, :ACTOR, :ADDRESS, :DEFENDANT;
	air:variable :DATA, :PURPOSE, :SPURPOSE, :PEVENT;
	air:rule :UDHR_1.

:UDHR_1 a air:BeliefRule;
       	air:label "Universal Declaration of Human Rights, Article 12 #1";
       	air:pattern {
          :COMPLAINT a tami:PrivacyViolationComplaint;
		tami:prevEvent :SEARCHEVENT;
		tami:actor :ACTOR;
		tami:defendant :DEFENDANT.
           :SEARCHEVENT a tami:SearchEvent.
	   :DEFENDANT a tami:Military.	
       	};
       air:description (:COMPLAINT " was filed by " :ACTOR " about " :SEARCHEVENT " performed by " :DEFENDANT );
	air:rule :UDHR_2.

:UDHR_2 a air:BeliefRule;
	air:label "Universal Declaration of Human Rights, Article 12 #2";
	air:pattern {
            :SEARCHEVENT tami:data :DATA;
		tami:purpose :SPURPOSE.
	    :DATA tami:purpose :PURPOSE.
	};
	air:description("Purpose of " :SEARCHEVENT " was " :SPURPOSE " and it used data meant to be used for " :PURPOSE " purposes ");
	air:rule :UDHR_3.

:UDHR_3 a air:BeliefRule;
        air:label "Universal Declaration of Human rights, Article 12 #4";
        air:pattern {
            :SPURPOSE owl:sameAs :PURPOSE
        };      
        air:description ("The purpose of the SearchEvent is the same as the purpose  of the data that was used for the Search Event");
        air:assert { :SEARCHEVENT air:compliant-with :Universal_Declaration_of_Human_Rights_Article12 };
	air:alt [ air:rule :UDHR_4 ].

:UDHR_4 a air:BeliefRule;
	air:pattern {
       		:SEARCHEVENT tami:prevEvent :PEVENT.
		:PEVENT a tami:Consent; tami:consenter :ACTOR.
        };      
        air:description ("As usage is inconsistent with purpose, consent " :PEVENT " was obtained from " :ACTOR);
        air:assert { :SEARCHEVENT air:compliant-with :Universal_Declaration_of_Human_Rights_Article12 };
	air:alt [ air:description ("No consent was obtained by " :DEFENDANT " before " :SEARCHEVENT " was performed "); 
                  air:rule :UDHR_5 ].

:UDHR_5 a air:BeliefRule;
	air:pattern {
        	:SEARCHEVENT tami:prevEvent :PEVENT.                        
		:PEVENT a tami:Notice; tami:actor :DEFENDANT; tami:notified :ACTOR.
        };
        air:description ("As usage of data was inconsistent with purpose, notice " :PEVENT " was given to  " :ACTOR);                
	air:assert { :SEARCHEVENT air:compliant-with :Universal_Declaration_of_Human_Rights_Article12 };
	air:alt [ air:description ( "No notice was given by " :DEFENDANT " before " :SEARCHEVENT " was performed ");
		  air:rule :UDHR_6 ].

:UDHR_6 a air:BeliefRule;
		air:pattern { };
		air:assert { :SEARCHEVENT air:non-compliant-with :Universal_Declaration_of_Human_Rights_Article12 };
        	air:description (:SEARCHEVENT " was performed without due process, making it incompliant with the Universal Declaration of Human Rights, Article 12").


# transitive closure of prevEvent
:trans-prevEvent a air:Policy;
    air:variable :E1, :E2, :E3;
    air:rule [
        air:label "Transitive closure of prevEvent";
        air:pattern { :E1 tami:prevEvent :E2.
                      :E2 tami:prevEvent :E3.
                     };
        air:assert { :E1 tami:prevEvent :E3 }
    ].



#ends
\end{verbatim}

An example event log it can run on appears at \url{http://dig.csail.mit.edu/2008/ARL/log.n3}.

\chapter{base-rules.ttl}
This file was written by Chris Hanson, collaborating with Gerry Sussman.
\label{base-rules}
\begin{verbatim}

# $Id: base-rules.ttl 8172 2007-12-13 19:01:57Z cph $
#
# Copyright (C) 2007 Massachusetts Institute of Technology
#
# This program is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# This program is distributed in the hope that it will be useful, but
# WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
# General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA
# 02110-1301, USA.

# AIR base rules

@prefix : <http://dig.csail.mit.edu/TAMI/2007/amord/base-rules#> .
@prefix abr: <http://dig.csail.mit.edu/TAMI/2007/amord/base-rules#> .

@prefix air: <http://dig.csail.mit.edu/TAMI/2007/amord/air#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix owl: <http://www.w3.org/2002/07/owl#> .

air:base-rules a air:Policy;
    air:rule
	:transitive-property-implication,
	:symmetric-property-implication,
	:sub-class-implication,
	:sub-property-implication,
	:same-as-implication,
	:domain-implication,
	:range-implication.

:transitive-property-implication a air:Hidden-rule;
    air:variable :P;
    air:pattern { :P a owl:TransitiveProperty. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :N1, :N2;
	air:pattern { :N1 :P :N2. };
	air:rule [
	    air:variable :N3;
	    air:pattern { :N1 :P :N3. };
	    air:matched-graph :G2;
	    air:rule [
		air:variable :N4;
		air:pattern { :N3 :P :N4. };
		air:matched-graph :G3;
		air:assertion [
		    air:statement { :N1 :P :N4. };
		    air:justification [
			air:rule-id :transitive-property-implication;
			air:antecedent :G1, :G2, :G3;
		    ];
		];
	    ];
	];
	air:rule [
	    air:variable :N3;
	    air:pattern { :N3 :P :N2. };
	    air:matched-graph :G2;
	    air:rule [
		air:variable :N4;
		air:pattern { :N4 :P :N3. };
		air:matched-graph :G3;
		air:assertion [
		    air:statement { :N4 :P :N2. };
		    air:justification [
			air:rule-id :transitive-property-implication;
			air:antecedent :G1, :G2, :G3;
		    ];
		];
	    ];
	];
    ].

:symmetric-property-implication a air:Hidden-rule;
    air:variable :P;
    air:pattern { :P a owl:SymmetricProperty. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :N1, :N2;
	air:pattern { :N1 :P :N2. };
	air:rule [
	    air:pattern { :N2 :P :N1. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :N1 :P :N2. };
		air:justification [
		    air:rule-id :symmetric-property-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ].

:sub-class-implication a air:Hidden-rule;
    air:variable :C1, :C2;
    air:pattern { :C1 rdfs:subClassOf :C2. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :N;
	air:pattern { :N a :C2. };
	air:rule [
	    air:pattern { :N a :C1. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :N a :C2. };
		air:justification [
		    air:rule-id :sub-class-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ].

:sub-property-implication a air:Hidden-rule;
    air:variable :P1, :P2;
    air:pattern { :P1 rdfs:subPropertyOf :P2. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :N1, :N2;
	air:pattern { :N1 :P2 :N2. };
	air:rule [
	    air:pattern { :N1 :P1 :N2. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :N1 :P2 :N2. };
		air:justification [
		    air:rule-id :sub-property-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ].

:same-as-implication a air:Hidden-rule;
    air:variable :N1, :N2;
    air:pattern { :N1 owl:sameAs :N2. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :P, :O;
	air:pattern { :N1 :P :O. };
	air:rule [
	    air:pattern { :N2 :P :O. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :N1 :P :O. };
		air:justification [
		    air:rule-id :same-as-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ];
    air:goal-rule [
	air:variable :S, :O;
	air:pattern { :S :N1 :O. };
	air:rule [
	    air:pattern { :S :N2 :O. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :S :N1 :O. };
		air:justification [
		    air:rule-id :same-as-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ];
    air:goal-rule [
	air:variable :S, :P;
	air:pattern { :S :P :N1. };
	air:rule [
	    air:pattern { :S :P :N2. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :S :P :N1. };
		air:justification [
		    air:rule-id :same-as-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ].

:domain-implication a air:Hidden-rule;
    air:variable :P, :C;
    air:pattern { :P rdfs:domain :C. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :N1;
	air:pattern { :N1 a :C. };
	air:rule [
	    air:variable :N2;
	    air:pattern { :N1 :P :N2. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :N1 a :C. };
		air:justification [
		    air:rule-id :domain-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ].

:range-implication a air:Hidden-rule;
    air:variable :P, :C;
    air:pattern { :P rdfs:range :C. };
    air:matched-graph :G1;
    air:goal-rule [
	air:variable :N1;
	air:pattern { :N1 a :C. };
	air:rule [
	    air:variable :N2;
	    air:pattern { :N2 :P :N1. };
	    air:matched-graph :G2;
	    air:assertion [
		air:statement { :N1 a :C. };
		air:justification [
		    air:rule-id :range-implication;
		    air:antecedent :G1, :G2;
		];
	    ];
	];
    ].
\end{verbatim}

\chapter{Useless Encoding as RDF}
\label{useless-rdf}
RDF is general enough to encode data in it that is not RDF at all. The following is a valid RDF document. 
\begin{verbatim}
:content = """
{\rtf1\mac\ansicpg10000\cocoartf824\cocoasubrtf440
{\fonttbl\f0\fswiss\fcharset77 Helvetica;}
{\colortbl;\red255\green255\blue255;}
\margl1440\margr1440\vieww9000\viewh8400\viewkind0
\pard\tx720\tx1440\tx2160\tx2880\tx3600\tx4320\tx5040\tx5760\tx6480\tx7200\tx792
0\tx8640\ql\qnatural\pardirnatural

\f0\fs24 \cf0 Hello}
"""^^foo:rtfDocument .
\end{verbatim}
This is not actually encoding our data as RDF, merely quoting it in another format. Further, we can even get rid of the strange literal, making a document that looks like
\begin{verbatim}
:content = (123, 92, 114, 116, 102, 49, 92, 109, 97, 99, 92, 97, 110, 115, 105,
 99, 112, 103, 49, 48, 48, 48, 48, 92, 99, 111, 99, 111, 97, 114, 116, 102, 56,
 50, 52, 92, 99, 111, 99, 111, 97, 115, 117, 98, 114, 116, 102, 52, 52, 48, 10,
 123, 92, 102, 111, 110, 116, 116, 98, 108, 92, 102, 48, 92, 102, 115, 119,
 105, 115, 115, 92, 102, 99, 104, 97, 114, 115, 101, 116, 55, 55, 32, 72, 101,
 108, 118, 101, 116, 105, 99, 97, 59, 125, 10, 123, 92, 99, 111, 108, 111, 114,
 116, 98, 108, 59, 92, 114, 101, 100, 50, 53, 53, 92, 103, 114, 101, 101, 110,
 50, 53, 53, 92, 98, 108, 117, 101, 50, 53, 53, 59, 125, 10, 92, 109, 97, 114,
 103, 108, 49, 52, 52, 48, 92, 109, 97, 114, 103, 114, 49, 52, 52, 48, 92, 118,
 105, 101, 119, 119, 57, 48, 48, 48, 92, 118, 105, 101, 119, 104, 56, 52, 48,
 48, 92, 118, 105, 101, 119, 107, 105, 110, 100, 48, 10, 92, 112, 97, 114, 100,
 92, 116, 120, 55, 50, 48, 92, 116, 120, 49, 52, 52, 48, 92, 116, 120, 50, 49,
 54, 48, 92, 116, 120, 50, 56, 56, 48, 92, 116, 120, 51, 54, 48, 48, 92, 116,
 120, 52, 51, 50, 48, 92, 116, 120, 53, 48, 52, 48, 92, 116, 120, 53, 55, 54,
 48, 92, 116, 120, 54, 52, 56, 48, 92, 116, 120, 55, 50, 48, 48, 92, 116, 120,
 55, 57, 50, 48, 92, 116, 120, 56, 54, 52, 48, 92, 113, 108, 92, 113, 110, 97,
 116, 117, 114, 97, 108, 92, 112, 97, 114, 100, 105, 114, 110, 97, 116, 117,
 114, 97, 108, 10, 10, 92, 102, 48, 92, 102, 115, 50, 52, 32, 92, 99, 102, 48,
 32, 72, 101, 108, 108, 111, 125) .
\end{verbatim}

\chapter{The Semantics of Alt}
\label{unstable.n3}
The following file is a reproduction of \uri{http://dig.csail.mit.edu/TAMI/2007/cwmrete/unstable.n3}. It models
\begin{eqnarray*}
\neg P & \to & Q \\
\neg Q & \to & P
\end{eqnarray*}
This is a subject of the many different semantics that have been defined for Prolog like languages.
\begin{verbatim}

#### Namespaces ####

# The default namespace is this document.
@prefix : <#> .

# AIR (AMORD in RDF) is the policy language.
@prefix air: <http://dig.csail.mit.edu/TAMI/2007/amord/air#> .

@prefix owl: <http://www.w3.org/2002/07/owl#>.

#### Policy ####

:MITProxCardPolicy a air:Policy;
    air:variable :S, :P, :O;
    air:rule [
	air:label "Rule 1";
	air:pattern {
	    :this :is :rule1
	};
        air:alt [
	    air:description ("It would seem that rule 1 failed to fire");
            air:assert { :rule2 :is :cool . :rule1 air:non-compliant-with owl:Thing }
	    ];
    ],
    [
	air:label "Rule 2";
	air:pattern {
	   :rule2 :is :cool
	};
        air:alt [
	    air:description ("It would seem that rule 2 failed to fire");
            air:assert { :this :is :rule1  . :rule2 air:non-compliant-with owl:Thing}
	    ];
    ] .
\end{verbatim}

After running the command \verb|python policyrunner.py test file:`pwd`/unstable.n3 file:`pwd`/unstable.n3|, the following output was created. 

\begin{verbatim}
     @prefix : <http://dig.csail.mit.edu/TAMI/2007/amord/tms#> .
    @prefix air: <http://dig.csail.mit.edu/TAMI/2007/amord/air#> .
    @prefix owl: <http://www.w3.org/2002/07/owl#> .
    @prefix prox: <file:/home/syosi/classes/meng-thesis/inst.n3#> .
    
    prox:rule1     air:non-compliant-with owl:Thing .
    
    <#_g0>     :justification :premise .
    {
        
        }     :justification :premise .
    {
        prox:rule1     air:non-compliant-with owl:Thing .
        
        }     :description  (
        "It would seem that rule 1 failed to fire" );
         :justification  [
             :antecedent-expr  [
                 a :And-justification;
                 :sub-expr <#_g0>,
                         [
                     air:closed-world-assumption  (
                    prox:MITProxCardPolicy
                    air:base-rules
                    <file:/home/syosi/classes/meng-thesis/inst.n3>
                    <http://dig.csail.mit.edu/TAMI/2007/amord/base-assumptions.ttl> );
                     :justification :premise ],
                        {} ];
             :rule-name <#_g0> ] .
    

\end{verbatim}

This shows exactly one of the two identical rules fired, which is unstable.
