diff --git a/alessio.txt b/alessio.txt
new file mode 100644
index 00000000000..ffa12cacac2
--- /dev/null
+++ b/alessio.txt
@@ -0,0 +1,36 @@
+Allocator.tlaps/tlapm_0803d7.smt
+Allocator.tlaps/tlapm_099ad8.smt
+Allocator.tlaps/tlapm_0a355e.smt
+Allocator.tlaps/tlapm_0ad495.smt
+Allocator.tlaps/tlapm_0b9140.smt
+Allocator.tlaps/tlapm_1d08e0.smt
+Allocator.tlaps/tlapm_2197e4.smt
+Allocator.tlaps/tlapm_23bce6.smt
+Allocator.tlaps/tlapm_3cbc97.smt
+Allocator.tlaps/tlapm_4222fc.smt
+Allocator.tlaps/tlapm_4561b7.smt
+Allocator.tlaps/tlapm_48700e.smt
+Allocator.tlaps/tlapm_4b71cb.smt
+Allocator.tlaps/tlapm_4d89a4.smt
+Allocator.tlaps/tlapm_50579e.smt
+Allocator.tlaps/tlapm_5473da.smt
+Allocator.tlaps/tlapm_5cb998.smt
+Allocator.tlaps/tlapm_5ef628.smt
+Allocator.tlaps/tlapm_6f89fe.smt
+Allocator.tlaps/tlapm_81962a.smt
+Allocator.tlaps/tlapm_81e00a.smt
+Allocator.tlaps/tlapm_9deec9.smt
+Allocator.tlaps/tlapm_a0df54.smt
+Allocator.tlaps/tlapm_ae2802.smt
+Allocator.tlaps/tlapm_ae2a83.smt
+Allocator.tlaps/tlapm_b01e66.smt
+Allocator.tlaps/tlapm_c42a04.smt
+Allocator.tlaps/tlapm_c85796.smt
+Allocator.tlaps/tlapm_ce8057.smt
+Allocator.tlaps/tlapm_dbde78.smt
+Allocator.tlaps/tlapm_dd19c4.smt
+Allocator.tlaps/tlapm_e03cb1.smt
+Allocator.tlaps/tlapm_e8eaa3.smt
+Allocator.tlaps/tlapm_f52471.smt
+Allocator.tlaps/tlapm_f84230.smt
+Allocator.tlaps/tlapm_fa32ac.smt
diff --git a/alethe-check.sh b/alethe-check.sh
index aef48065487..04476e174c7 100755
--- a/alethe-check.sh
+++ b/alethe-check.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 
 # tfile="$(mktemp /tmp/foo.XXXXXXXXX)" || exit 1
-tfile="/home/hbarbosa/cvc/wt-proofnew/pf.alethe"
+tfile="/home/hbarbosa/cvc5/wt-alethe/test.alethe"
 
-./prod/bin/cvc5 --proof-format-mode=alethe --proof-granularity=theory-rewrite --lang=smt2 --dump-proofs --proof-alethe-res-pivots --dag-thresh=0  $@ | tail -n +2 > $tfile
-carcara check --allow-int-real-subtyping --expand-let-bindings --skip-unknown-rules $tfile $1
+./prod/bin/cvc5 --proof-format=alethe --lang=smt2 --dump-proofs --dag-thresh=0  $@ | tail -n +2 > $tfile
+~/carcara/target/release/carcara check --no-print-with-sharing --allow-int-real-subtyping --expand-let-bindings -i $tfile $1
diff --git a/allrun.sh b/allrun.sh
index 04f1c2cfdb4..f93b0260567 100755
--- a/allrun.sh
+++ b/allrun.sh
@@ -4,8 +4,8 @@ options="--tlimit=1500 --simplification=none --full-saturate-quant --no-stats"
 traces=""
 time=""
 ulimit="ulimit -S -t 10"
-file="isabelle-mirabelle.txt"
-path="/home/hbarbosa/benchmarks/isabelle-mirabelle/"
+file="alessio.txt"
+path="/home/hbarbosa/cvc5/wt-alethe/"
 
 echo "Options: $options"
 echo "Traces: $traces"