diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 8baa5b519540bb918fa39575a915351d01b0bf2f..6350d497eea0592a2ef6273e6dd0059fef40a809 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -1,5 +1,7 @@
 .. _acas_xu:
 
+Written in november 2022
+
 ACAS-Xu
 *******
 
@@ -62,7 +64,7 @@ There are several functional properties one may want to verify on this system, f
 * guarantee that the system will not output a Strong advisory where a Weak variant would be enough
 
 Authors of [Katz2017]_ propose ten properties to verify. We
-will reproduce the first here, and try to check whether a
+will reproduce the two first here, and try to check whether a
 given neural network respects it. 
 
 **property** 
@@ -81,6 +83,22 @@ given neural network respects it.
 
    * :math:`COC` ≤ 1500
 
+**property** 
+    :math:`\phi_2`
+
+**definition**
+    If the intruder is distant and is significantly slower than the ownship, the score of a COC advisory will never be maximal.
+
+**input constraints**
+
+   * :math:`\rho` ≥ 55947.691
+   * :math:`v_{own}` ≥ 1145
+   * :math:`v_{int}` ≤ 60
+
+**desired output property**
+
+   * :math:`COC` is not the maximum
+
 Modelling the problem using WhyML
 ---------------------------------
 
@@ -122,6 +140,7 @@ Internally, when provided with a neural network file, CAISAR will perform some b
 If those checks pass, then CAISAR will internally build a theory, named as the original neural network. This theory will contain two subtheories that provide
 logical symbols we can use in our theory: ``AsTuple`` and ``AsArray``.
 We will only consider the ``AsTuple`` subtheory for this tutorial.
+CAISAR currently supports neural network in ONNX and NNet format.
 
 This theory is equivalent to the following WhyML file:
 
@@ -164,6 +183,12 @@ property :math:`\phi_1`. We define all floating points inputs
 :math:`x_i` for :math:`i \in (0..4)` that respect the
 properties defined in :math:`\phi_1` (in WhyML, ``->`` stands for
 the logical implication).
+For the neural network we consider, 
+:math:`x_0 = \rho, x_1 = \theta, x_2 = \psi, x_3 = v_{own},
+x_4 = v_{int}`.
+According to the original authors, values were normalized
+during the network's training: we adapt the values they provide in
+their `repository <https://github.com/NeuralNetworkVerification/Marabou/tree/master/resources/properties>`_.
 
 .. code-block:: ocaml
   
@@ -202,19 +227,27 @@ The final file looks like this:
 
 This file is available as is, under the example folder of our repo: `property_1.why <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/property_1.why>`_.
 A neural network in NNet format that should respect this
-property is available here: `ACASXU_1_1.nnet <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/ACASXU_1_1.nnet>`_ (from the Marabou repository).
+property is available here: `ACASXU_1_1.nnet <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/ACASXU_1_1.nnet>`_.
 
 
 Checking the property with CAISAR
 ---------------------------------
 
-Assuming the chosen prover is on your path and you are in
-CAISAR's root, you may launch caisar using the following command line:
+Once we have a formalization of our verification problem,
+it is time to launch CAISAR on it. We will use the ``-L``
+option to specify the location of our neural network files.
+Refer to `usage`_ for a more in depth description of CAISAR
+usage.
+We will use the `Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_ prover, as it is publicly available. Please refer to the above link
+to install the tool.
 
+Assuming Marabou is on your path and you are in
+CAISAR's root, you may launch caisar using the following command line
 
 .. code-block:: bash
 
-    caisar verify --prover Marabou -L examples/acasxu/nets/ --format whyml examples/acasxu/property_1.why -vv -t 10m
+    caisar verify --prover Marabou -L examples/acasxu/nets/ --format whyml examples/acasxu/property_1.why -t 10m
+
 
 Take note that this may take some time, depending to your
 machine.
@@ -222,6 +255,30 @@ machine.
 CAISAR will return you either ``Valid``, ``Invalid`` or
 ``Timeout``
 
+Using First-Order Logic constructs
+----------------------------------
+
+Let us verify property :math:`\phi_2`. The main difference
+is the condition on the output: that COC should not be the
+max value. A straightforward way to express this property is
+that :math:`y_0` is below at least one other output.
+In first-order logic, we can describe this as a disjunction
+of clauses:
+":math:`y_0 \leq y_1` or  :math:`y_0 \leq y_2` or :math:`y_0 \leq y_3` or 
+:math:`y_0 \leq y_4`". 
+This translates in WhyML as the following (``\/`` stands for
+the disjunction):
+
+.. code-block:: ocaml
+    
+    y0 .< y1 \/ y0 .< y2 \/ y0 .< y3 \/ y0 .< y4
+
+We can then verify the resulting verification problem as
+before:
+
+.. code-block:: bash
+
+    caisar verify --prover Marabou -L examples/acasxu/nets/ --format whyml examples/acasxu/property_2.why -t 10m
 
 
 References