diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
new file mode 100644
index 0000000..a1ed0b8
--- /dev/null
+++ b/.github/workflows/test.yml
@@ -0,0 +1,62 @@
+name: Test All Rules
+
+on:
+  push:
+    paths:
+      - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java'
+  pull_request:
+    paths:
+      - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java'
+
+jobs:
+  test-all-rules:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Set up Java
+        uses: actions/setup-java@v4
+        with:
+          java-version: '23'
+          distribution: 'temurin'
+
+      - name: Cache Maven dependencies
+        uses: actions/cache@v3
+        with:
+          path: ~/.m2/repository
+          key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+          restore-keys: |
+            ${{ runner.os }}-maven-
+
+      - name: Build project
+        run: mvn -B compile --file pom.xml
+
+      - name: Generate JSON for all rules
+        run: |
+          mkdir -p tmp-rules
+          mvn dependency:resolve
+          chmod +x scripts/generate-rule-json.sh
+          ./scripts/generate-rule-json.sh
+
+      - name: Install dependencies
+        run: |
+          chmod +x scripts/install-dependencies.sh
+          ./scripts/install-dependencies.sh
+
+      - name: Build qed-prover
+        run: |
+          chmod +x scripts/build-qed-prover.sh
+          ./scripts/build-qed-prover.sh
+
+      - name: Test all rules
+        run: |
+          chmod +x scripts/test-rules.sh
+          ./scripts/test-rules.sh
+
+      - name: Upload test artifacts
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: results
+          path: tmp-rules/
\ No newline at end of file
diff --git a/pom.xml b/pom.xml
index ccfa971..fd29e81 100644
--- a/pom.xml
+++ b/pom.xml
@@ -103,9 +103,9 @@
             <version>0.67.0</version>
         </dependency>
         <dependency>
-            <groupId>io.github.cvc5</groupId>
+            <groupId>io.github.p-org.solvers</groupId>
             <artifactId>cvc5</artifactId>
-            <version>1.2.1</version>
+            <version>0.0.7-v5</version>
         </dependency>
         <dependency>
             <groupId>org.reflections</groupId>
@@ -113,4 +113,4 @@
             <version>0.10.2</version>
         </dependency>
     </dependencies>
-</project>
+</project>
\ No newline at end of file
diff --git a/scripts/build-qed-prover.sh b/scripts/build-qed-prover.sh
new file mode 100644
index 0000000..10fe4b0
--- /dev/null
+++ b/scripts/build-qed-prover.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+# Build qed-prover with Rust nightly
+
+curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly
+source $HOME/.cargo/env
+
+git clone https://github.com/qed-solver/prover.git qed-prover
+cd qed-prover
+cargo +nightly build --release
\ No newline at end of file
diff --git a/scripts/generate-rule-json.sh b/scripts/generate-rule-json.sh
new file mode 100644
index 0000000..a34f5da
--- /dev/null
+++ b/scripts/generate-rule-json.sh
@@ -0,0 +1,45 @@
+#!/bin/bash
+
+# Script to generate JSON files for all RRule instances
+
+# Create temporary Java file for JSON generation
+cat > JsonGenerator.java << 'EOF'
+import org.qed.*;
+import com.fasterxml.jackson.databind.ObjectMapper;
+import com.fasterxml.jackson.databind.node.ObjectNode;
+import java.nio.file.*;
+
+public class JsonGenerator {
+    public static void main(String[] args) throws Exception {
+        String className = args[0];
+        Class<?> clazz = Class.forName(className);
+        RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance();
+        ObjectMapper mapper = new ObjectMapper();
+        String fileName = rule.name() + "-" + rule.info() + ".json";
+        ObjectNode jsonNode = rule.toJson();
+        mapper.writerWithDefaultPrettyPrinter().writeValue(
+            Path.of("tmp-rules", fileName).toFile(),
+            jsonNode
+        );
+    }
+}
+EOF
+
+# Build classpath
+MAVEN_CP=$(mvn dependency:build-classpath -Dmdep.outputFile=/dev/stdout -q)
+CLASSPATH="target/classes:${MAVEN_CP}"
+
+# Compile the generator
+javac -cp "$CLASSPATH" JsonGenerator.java
+
+# Generate JSON for each rule
+find src/main/java/org/qed/Generated/RRuleInstances -name '*.java' | while read file; do
+    className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||')
+    echo "Generating JSON for: $className"
+    java -cp ".:$CLASSPATH" JsonGenerator "$className"
+done
+
+# Cleanup
+rm -f JsonGenerator.java JsonGenerator.class
+
+echo "JSON generation complete. Files are in tmp-rules/"
\ No newline at end of file
diff --git a/scripts/install-dependencies.sh b/scripts/install-dependencies.sh
new file mode 100644
index 0000000..500879f
--- /dev/null
+++ b/scripts/install-dependencies.sh
@@ -0,0 +1,17 @@
+#!/bin/bash
+
+# Install required dependencies for qed-prover
+
+sudo apt-get update
+sudo apt-get install -y jq z3
+
+# Install cvc5 - try package manager first, otherwise build from source
+sudo apt-get install -y cvc5 || (
+    sudo apt-get install -y cmake libgmp-dev &&
+    git clone --depth 1 https://github.com/cvc5/cvc5.git &&
+    cd cvc5 &&
+    ./configure.sh --auto-download &&
+    cd build &&
+    make -j$(nproc) &&
+    sudo make install
+)
\ No newline at end of file
diff --git a/scripts/test-rules.sh b/scripts/test-rules.sh
new file mode 100644
index 0000000..5dc149b
--- /dev/null
+++ b/scripts/test-rules.sh
@@ -0,0 +1,33 @@
+#!/bin/bash
+
+# Test all generated rules with qed-prover
+
+echo "## QED Prover Test Results" >> $GITHUB_STEP_SUMMARY
+echo "" >> $GITHUB_STEP_SUMMARY
+
+failed_rules=""
+total_count=0
+passed_count=0
+
+for json_file in tmp-rules/*.json; do
+    rule_name=$(basename "$json_file" .json)
+    total_count=$((total_count + 1))
+    ./qed-prover/target/release/qed-prover "$json_file" || true
+    
+    result_file="${json_file%.json}.result"
+    if [ -f "$result_file" ] && jq -e '.provable == true' "$result_file" > /dev/null 2>&1; then
+        echo "✅ $rule_name: PASSED" >> $GITHUB_STEP_SUMMARY
+        passed_count=$((passed_count + 1))
+    else
+        echo "❌ $rule_name: FAILED" >> $GITHUB_STEP_SUMMARY
+        failed_rules="$failed_rules$rule_name,"
+    fi
+done
+
+echo "" >> $GITHUB_STEP_SUMMARY
+echo "**Summary:** $passed_count/$total_count passed" >> $GITHUB_STEP_SUMMARY
+
+if [ -n "$failed_rules" ]; then
+    echo "::error::Failed rules: ${failed_rules%,}"
+    exit 1
+fi
\ No newline at end of file
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/JoinAssociate.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinAssociate.java
similarity index 100%
rename from src/main/java/org/qed/Generated/RRuleInstances/JoinAssociate.java
rename to src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinAssociate.java
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/JoinCommute.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinCommute.java
similarity index 100%
rename from src/main/java/org/qed/Generated/RRuleInstances/JoinCommute.java
rename to src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinCommute.java
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinJoinTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinJoinTranspose.java
similarity index 100%
rename from src/main/java/org/qed/Generated/RRuleInstances/SemiJoinJoinTranspose.java
rename to src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinJoinTranspose.java
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinProjectTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinProjectTranspose.java
similarity index 100%
rename from src/main/java/org/qed/Generated/RRuleInstances/SemiJoinProjectTranspose.java
rename to src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinProjectTranspose.java
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinRemove.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinRemove.java
similarity index 100%
rename from src/main/java/org/qed/Generated/RRuleInstances/SemiJoinRemove.java
rename to src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinRemove.java
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java
index 24165aa..d16f8ef 100644
--- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java
+++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java
@@ -19,7 +19,7 @@ public RelRN before() {
         var join = left.join(JoinRelType.INNER, joinCond, right);
         return join.filter("outer");
     }
-
+    
     @Override
     public RelRN after() {
         return left.join(JoinRelType.INNER, RexRN.and(joinCond, left.joinPred("outer", right)), right);
diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java
index d1bc90e..790c1d2 100644
--- a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java
+++ b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java
@@ -17,13 +17,11 @@ public record SemiJoinFilterTranspose() implements RRule {
 
     @Override
     public RelRN before() {
-        // Semi-join followed by a filter
         return left.join(JoinRelType.SEMI, joinCond, right).filter(filterPred);
     }
 
     @Override
     public RelRN after() {
-        // Push the filter before the semi-join
         RelRN leftFiltered = left.filter(filterPred);
         return leftFiltered.join(JoinRelType.SEMI, leftFiltered.joinPred("join", right), right);
     }