diff --git a/src/examples/bimetatrans/README.md b/src/examples/bimetatrans/README.md
new file mode 100644
index 00000000..d47e5e13
--- /dev/null
+++ b/src/examples/bimetatrans/README.md
@@ -0,0 +1,218 @@
+### BiMetaTrans 1.0
+
+BiMetaTrans(Prolog, RuleML) is a bidirectional translator capable of
+parsing and generating a well-formed sublanguage of RuleML/XML to/from
+a metalogical encoding of our own design called Prolog/'$V'. For later
+ease of reference:
+
+* Prolog/'$V' stands for "Metalogic Prolog with variable-as-'$V'-term encoding"
+* RuleML/XML stands for "RuleML in XML with any kind of rendering"
+* RuleML/xmL stands for "RuleML in minified XML"
+* RuleML/Xml stands for "RuleML in indented XML"
+
+"Minified XML" refers to XML with only necessary whitespace, between
+element names and attributes, and pairs of attributes, with all
+indentation stripped out. "Indented XML" contains indentation and
+newlines, and is usually formatted for human readers.
+
+The specification of Prolog/'$V', and of the NafHornlogEq sublanguage
+of RuleML/XML targeted by BiMetaTrans, is contained in the preprint
+[Invertible Bidirectional Metalogical Translation Between Prolog and
+RuleML/XML for Knowledge Representation and
+Querying](http://ruleml.org/papers/RuleMLXMLBiDirTransScryer.pdf) and
+its accompanying talk
+[slides](http://ruleml.org/talks/RuleMLXMLBiDirTransScryer-talk.pdf). The
+preprint and talk also describe the implementation of BiMetaTrans
+found here, and outlines a strategy for proving the invertibility of
+BiMetaTrans.
+
+BiMetaTrans exports a single public predicate subsuming its user
+API, `parse_ruleml/3`. It has two modes, each corresponding to a single
+direction of translation:
+
+```
+parse_ruleml(+AssertItems, +QueryItems, ?XML) (Prolog->RuleML)
+parse_ruleml(?AssertItems, ?QueryItems, +XML) (RuleML->Prolog)
+```
+
+The modes constrain the inputs to fit one of two patterns, the
+first where AssertItems and QueryItems are instantiated and XML is
+possibly a variable, and conversely for the second. Instantiated
+inputs are expected to be ground, meaning they should not contain
+free variables.
+
+We explore several examples of its use in Scryer Prolog.
+
+Loading BiMetaTrans from the Scryer REPL:
+
+```
+?- use_module('src/examples/bimetatrans/bimetatrans').
+```
+
+Using `write/1` to print the string to standard output (`write/1` is used
+because it does not print strings with escape characters (ie. `\"` for
+double quote)):
+
+```
+?- parse_ruleml([people('Alex',male),people('Alex',female),people('Siri',female)], [], XML),
+ write(XML).
+"peopleAlexmalepeopleAlexfemalepeopleSirifemale" XML = "\
+ \
+ people\
+ Alex\
+ male\
+ \
+ \
+ people\
+ Alex\
+ female\
+ \
+ \
+ people\
+ Siri\
+ female\
+ \
+ ").
+ AssertItems = [people('Alex',male),people('Alex',female),people('Siri',female)], QueryItems = [].
+```
+
+Non-empty AssertItems and QueryItems lists generated to RuleML/xmL
+simultaneously:
+
+```
+?- parse_ruleml([a(item), b(item), c(item)], [(?- p, q, r(1), s(-2.222342432), t("attached")), (?- u, v('$V'(q)))], XML),
+ write(XML).
+"aitembitemcitempqr1s-2.222342432t"attached"uvq" XML = "aitembitemcitempqr1s-2.222342432t\"attached\"uvq" XML = "
+
+ a
+ item
+
+
+ b
+ item
+
+
+ c
+ item
+
+
+
+
+
+ p
+
+
+ q
+
+
+ r
+ 1
+
+
+ s
+ -2.222342432
+
+
+ t
+ \"attached\"
+
+
+
+
+
+
+ u
+
+
+ v
+ q
+
+
+
+```
+
+The AssertItems and QueryItems lists can then be recovered using this
+RuleML/Xml string, with the `\` character added to the end of each
+line:
+
+```
+?- parse_ruleml(AssertItems, QueryItems,
+ "\
+ \
+ a\
+ item\
+ \
+ \
+ b\
+ item\
+ \
+ \
+ c\
+ item\
+ \
+ \
+ \
+ \
+ \
+ p\
+ \
+ \
+ q\
+ \
+ \
+ r\
+ 1\
+ \
+ \
+ s\
+ -2.222342432\
+ \
+ \
+ t\
+ \"attached\"\
+ \
+ \
+ \
+ \
+ \
+ \
+ u\
+ \
+ \
+ v\
+ q\
+ \
+ \
+ ").
+ AssertItems = [a(item),b(item),c(item)], QueryItems = [(?-p,q,r(1),s(-2.222342432),t("attached")),(?-u,v('$V'(q)))].
+```
diff --git a/src/examples/bimetatrans/bimetatrans.pl b/src/examples/bimetatrans/bimetatrans.pl
index d652d651..cc894065 100644
--- a/src/examples/bimetatrans/bimetatrans.pl
+++ b/src/examples/bimetatrans/bimetatrans.pl
@@ -19,8 +19,8 @@
* all indentation stripped out. "Indented XML" contains indentation
* and newlines, and is usually formatted for human readers.
*
- * parse_ruleml/3 is the sole public predicate of BiMetaTrans(RuleML,
- * Prolog), a bidirectional translator capable of parsing well-formed
+ * parse_ruleml/3 is the sole public predicate of BiMetaTrans(Prolog,
+ * RuleML), a bidirectional translator capable of parsing well-formed
* RuleML/XML (valid w.r.t. a proposed anchor schema nafhornlogeq
* defining a sublanguage of the existing anchor schema naffologeq) to
* an equivalent Prolog/'$V' term and back to RuleML/xmL. It has the