diff --git a/acasxu.why b/acasxu.why
new file mode 100644
index 0000000000000000000000000000000000000000..33c6ee6e44fc4c21ead159748fcf688e10e2fed5
--- /dev/null
+++ b/acasxu.why
@@ -0,0 +1,22 @@
+theory ACAS_XU_P1
+
+  use real.Real
+
+  constant x0:real
+  axiom x0: 0.6 <= x0 <= 0.6798577687
+  
+  constant x1:real
+  axiom x1: -0.5 <= x1 <= 0.5
+  
+  constant x2:real
+  axiom x2: -0.5 <= x2 <= 0.5
+  
+  constant x3:real
+  axiom x3: 0.45 <= x3 <= 0.5
+  
+  constant x4:real
+  axiom x4: -0.5 <= x4 <= -0.45
+  
+  goal P1: forall y0:real. y0 <= 3.9911256459
+
+end