diff --git a/proofs/eo/cpc/examples/now.eo b/proofs/eo/cpc/examples/now.eo
new file mode 100644
index 00000000000..87b95a19464
--- /dev/null
+++ b/proofs/eo/cpc/examples/now.eo
@@ -0,0 +1,6 @@
+unsat
+(define @t1 () (str.in_re "a" (str.to_re "b")))
+(assume @p1 @t1)
+(step @p2 :rule str-in-re-consume :args ((= @t1 false)))
+(step @p3 false :rule eq_resolve :premises (@p1 @p2))
+
diff --git a/proofs/eo/cpc/examples/now.ep b/proofs/eo/cpc/examples/now.ep
new file mode 100644
index 00000000000..821e5d95530
--- /dev/null
+++ b/proofs/eo/cpc/examples/now.ep
@@ -0,0 +1,12 @@
+(include "../rules/Booleans.eo")
+(include "../theories/Ints.eo")
+(include "../programs/Arith.eo")
+(include "../theories/Strings.eo")
+(include "../rules/Strings.eo")
+(include "../programs/Strings.eo")
+(include "../rules/Strings.eo")
+(define @t1 () (str.in_re "a" (str.to_re "b")))
+(assume @p1 @t1)
+(step @p2 :rule str-in-re-consume :args ((= @t1 false)))
+(step @p3 false :rule eq_resolve :premises (@p1 @p2))
+
diff --git a/proofs/eo/cpc/examples/reg_eval.eo b/proofs/eo/cpc/examples/reg_eval.eo
new file mode 100644
index 00000000000..f229efa2718
--- /dev/null
+++ b/proofs/eo/cpc/examples/reg_eval.eo
@@ -0,0 +1,5 @@
+(define @t1 () (str.in_re "a" (str.to_re "b")))
+(assume @p1 @t1)
+(step @p2 :rule str-in-re-consume :args ((= @t1 false)))
+(step @p3 false :rule eq_resolve :premises (@p1 @p2))
+
diff --git a/proofs/eo/cpc/examples/reg_eval.smt2 b/proofs/eo/cpc/examples/reg_eval.smt2
new file mode 100644
index 00000000000..099ea6a8264
--- /dev/null
+++ b/proofs/eo/cpc/examples/reg_eval.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+(assert (str.in_re "a" (str.to_re "b")))
+(check-sat)
diff --git a/proofs/eo/cpc/examples/run.sh b/proofs/eo/cpc/examples/run.sh
new file mode 100755
index 00000000000..da566124191
--- /dev/null
+++ b/proofs/eo/cpc/examples/run.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+
+# first input -- cvc5 binary
+# second input -- ethos binary
+
+# prepend includes
+echo (include "theories/Ints.eo") > reg_eval.eo
+echo (include "programs/Arith.eo") > reg_eval.eo
+echo (include "theories/Strings.eo") > reg_eval.eo 
+echo (include "rules/Strings.eo") > reg_eval.eo
+echo (include "programs/Strings.eo") > reg_eval.eo
+echo (include "rules/Strings.eo") > reg_eval.eo
+
+# produce proof (remove `unsat` line)
+$1 --dump-proofs --proof-format-mode=cpc --proof-granularity=dsl-rewrite reg_eval.smt2 | tail -n +2 > reg_eval.eo 
+
+
+
+# check the proof
+$2 reg_eval.eo
+
+# check another proof
+ethos tmp.eo
diff --git a/proofs/eo/cpc/examples/tmp.eo b/proofs/eo/cpc/examples/tmp.eo
new file mode 100644
index 00000000000..c644be12aa7
--- /dev/null
+++ b/proofs/eo/cpc/examples/tmp.eo
@@ -0,0 +1,9 @@
+(include "theories/Ints.eo")
+(include "programs/Arith.eo")
+(include "theories/Strings.eo")
+(include "rules/Strings.eo")
+(include "programs/Strings.eo")
+(include "rules/Strings.eo")
+
+(step @p1 (= (str.in_re "s" (str.to_re "s")) true) :rule str-in-re-eval :args ((= (str.in_re "s" (str.to_re "s")) true)))
+