diff --git a/proofs/pipeline/examples/run.expected b/proofs/pipeline/examples/run.expected
index 2c1c0eac2a0f6e92b7cd5cde66636f6b1154cbcf..e3eae81838984cd5d539a2252502ee623e3e612c 100644
--- a/proofs/pipeline/examples/run.expected
+++ b/proofs/pipeline/examples/run.expected
@@ -1,6 +1,24 @@
-symbol hello!1 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q)))));
-symbol hello!2 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q)))));
-symbol hello!3 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q)))));
-symbol hello!4 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q)))));
-symbol hello!5 : @Prf (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q)));
-symbol hello!6 : @Prf (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q)));
\ No newline at end of file
+symbol hello!1 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q))))) ≔
+begin
+  why3;
+end;
+symbol hello!2 : @Prf (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (@imp (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))) (imp spec.main.P (imp spec.main.Q (conj spec.main.P spec.main.Q))))) ≔
+begin
+  why3;
+end;
+symbol hello!3 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))))) ≔
+begin
+  why3;
+end;
+symbol hello!4 : @Prf (@imp (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) (@imp (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) (disj (not spec.main.P) (disj (not spec.main.Q) (conj spec.main.P spec.main.Q))))) ≔
+begin
+  why3;
+end;
+symbol hello!5 : @Prf (disj spec.main.P (disj (not spec.main.P) (not spec.main.Q))) ≔
+begin
+  why3;
+end;
+symbol hello!6 : @Prf (disj spec.main.Q (disj (not spec.main.P) (not spec.main.Q))) ≔
+begin
+  why3;
+end;
\ No newline at end of file
diff --git a/proofs/pipeline/pipe.ml b/proofs/pipeline/pipe.ml
index 63846b4f9754d91ba08d81775660984f823db435..6aa85f134fe9a115134bf6dbb517743478485b68 100644
--- a/proofs/pipeline/pipe.ml
+++ b/proofs/pipeline/pipe.ml
@@ -27,7 +27,8 @@ let process proveit src qfo_conf encoding specification =
         "require open spec.main;";
       ]
   and chainprops depfile = process "psnj-chainprops" [ depfile ]
-  and appaxiom = process "psnj-appaxiom" [ "-a"; "Prf" ] in
+  and appaxiom = process "psnj-appaxiom" [ "-a"; "Prf" ] 
+  and solve = process "psnj-autosolve" [ "--fixed" ] in
   (* Set some file names *)
   let logfile =
     (* File produced by proveit if proveit is provided, src otherwise *)
@@ -44,7 +45,7 @@ let process proveit src qfo_conf encoding specification =
   run (echo json |. mkdeps |. dopth > depfile);
   let sttprops =
     collect stdout
-      (echo json |. mkprops |. foise |. chainprops depfile |. appaxiom)
+      (echo json |. mkprops |. foise |. chainprops depfile |. appaxiom |. solve)
   in
   Format.printf "%s" sttprops