diff --git a/carcara/src/checker/rules/clausification.rs b/carcara/src/checker/rules/clausification.rs
index 0da424f9..a23a142c 100644
--- a/carcara/src/checker/rules/clausification.rs
+++ b/carcara/src/checker/rules/clausification.rs
@@ -1,6 +1,7 @@
 use super::{
-    assert_clause_len, assert_eq, assert_is_expected, assert_num_premises, assert_operation_len,
-    assert_polyeq_expected, get_premise_term, CheckerError, EqualityError, RuleArgs, RuleResult,
+    assert_clause_len, assert_eq, assert_is_expected, assert_num_args, assert_num_premises,
+    assert_operation_len, assert_polyeq_expected, get_premise_term, CheckerError, EqualityError,
+    RuleArgs, RuleResult,
 };
 use crate::ast::*;
 use indexmap::IndexMap;
@@ -59,37 +60,33 @@ pub fn distinct_elim(RuleArgs { conclusion, pool, .. }: RuleArgs) -> RuleResult
     }
 }
 
-pub fn and(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
+pub fn and(RuleArgs { conclusion, premises, args, .. }: RuleArgs) -> RuleResult {
     assert_num_premises(premises, 1)?;
+    assert_num_args(args, 1)?;
     assert_clause_len(conclusion, 1)?;
 
     let and_term = get_premise_term(&premises[0])?;
     let and_contents = match_term_err!((and ...) = and_term)?;
 
-    if !and_contents.contains(&conclusion[0]) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::And,
-            conclusion[0].clone(),
-        ));
-    }
-    Ok(())
+    assert_eq(
+        &conclusion[0],
+        &and_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
+    )
 }
 
-pub fn not_or(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
+pub fn not_or(RuleArgs { conclusion, premises, args, .. }: RuleArgs) -> RuleResult {
     assert_num_premises(premises, 1)?;
+    assert_num_args(args, 1)?;
     assert_clause_len(conclusion, 1)?;
 
     let or_term = get_premise_term(&premises[0])?;
     let or_contents = match_term_err!((not (or ...)) = or_term)?;
     let conclusion = conclusion[0].remove_negation_err()?;
 
-    if !or_contents.contains(conclusion) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::Or,
-            conclusion.clone(),
-        ));
-    }
-    Ok(())
+    assert_eq(
+        conclusion,
+        &or_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
+    )
 }
 
 pub fn or(RuleArgs { conclusion, premises, .. }: RuleArgs) -> RuleResult {
@@ -464,13 +461,13 @@ mod tests {
             ",
             "Simple working examples" {
                 "(assume h1 (and p q))
-                (step t2 (cl q) :rule and :premises (h1))": true,
+                (step t2 (cl q) :rule and :premises (h1) :args (1))": true,
 
                 "(assume h1 (and p q r s))
-                (step t2 (cl p) :rule and :premises (h1))": true,
+                (step t2 (cl p) :rule and :premises (h1) :args (0))": true,
 
                 "(assume h1 (and p q r s))
-                (step t2 (cl s) :rule and :premises (h1))": true,
+                (step t2 (cl s) :rule and :premises (h1) :args (3))": true,
             }
             "Number of premises != 1" {
                 "(step t1 (cl p) :rule and)": false,
@@ -481,22 +478,22 @@ mod tests {
             }
             "Premise clause has more than one term" {
                 "(step t1 (cl (and p q) (and r s)) :rule hole)
-                (step t2 (cl p) :rule and :premises (t1))": false,
+                (step t2 (cl p) :rule and :premises (t1) :args (0))": false,
             }
             "Conclusion clause does not have exactly one term" {
                 "(assume h1 (and p q r s))
-                (step t2 (cl q s) :rule and :premises (h1))": false,
+                (step t2 (cl q s) :rule and :premises (h1) :args (1))": false,
 
                 "(assume h1 (and p q))
-                (step t2 (cl) :rule and :premises (h1))": false,
+                (step t2 (cl) :rule and :premises (h1) :args (0))": false,
             }
             "Premise is not an \"and\" operation" {
                 "(assume h1 (or p q r s))
-                (step t2 (cl r) :rule and :premises (h1))": false,
+                (step t2 (cl r) :rule and :premises (h1) :args (0))": false,
             }
             "Conclusion term is not in premise" {
                 "(assume h1 (and p q r))
-                (step t2 (cl s) :rule and :premises (h1))": false,
+                (step t2 (cl s) :rule and :premises (h1) :args (0))": false,
             }
         }
     }
@@ -512,28 +509,28 @@ mod tests {
             ",
             "Simple working examples" {
                 "(assume h1 (not (or p q)))
-                (step t2 (cl (not q)) :rule not_or :premises (h1))": true,
+                (step t2 (cl (not q)) :rule not_or :premises (h1) :args (1))": true,
 
                 "(assume h1 (not (or p q r s)))
-                (step t2 (cl (not p)) :rule not_or :premises (h1))": true,
+                (step t2 (cl (not p)) :rule not_or :premises (h1) :args (0))": true,
             }
             "Conclusion clause is of the wrong form" {
                 "(assume h1 (not (or p q r s)))
-                (step t2 (cl (not q) (not s)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not q) (not s)) :rule not_or :premises (h1) :args (1))": false,
 
                 "(assume h1 (not (or p q)))
-                (step t2 (cl q) :rule not_or :premises (h1))": false,
+                (step t2 (cl q) :rule not_or :premises (h1) :args (1))": false,
             }
             "Premise is of the wrong form" {
                 "(assume h1 (not (and p q r s)))
-                (step t2 (cl (not r)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not r)) :rule not_or :premises (h1) :args (2))": false,
 
                 "(assume h1 (or p q r s))
-                (step t2 (cl (not r)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not r)) :rule not_or :premises (h1) :args (2))": false,
             }
             "Conclusion term is not in premise" {
                 "(assume h1 (not (or p q r)))
-                (step t2 (cl (not s)) :rule not_or :premises (h1))": false,
+                (step t2 (cl (not s)) :rule not_or :premises (h1) :args (0))": false,
             }
         }
     }
diff --git a/carcara/src/checker/rules/tautology.rs b/carcara/src/checker/rules/tautology.rs
index ecbd17db..c7d278ae 100644
--- a/carcara/src/checker/rules/tautology.rs
+++ b/carcara/src/checker/rules/tautology.rs
@@ -1,6 +1,6 @@
 use super::{
-    assert_clause_len, assert_eq, assert_num_premises, assert_polyeq, get_premise_term,
-    CheckerError, RuleArgs, RuleResult,
+    assert_clause_len, assert_eq, assert_num_args, assert_num_premises, assert_polyeq,
+    get_premise_term, CheckerError, RuleArgs, RuleResult,
 };
 use crate::{ast::*, checker::rules::assert_operation_len};
 
@@ -31,17 +31,16 @@ pub fn not_not(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
     assert_eq(p, &conclusion[1])
 }
 
-pub fn and_pos(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
+pub fn and_pos(RuleArgs { conclusion, args, .. }: RuleArgs) -> RuleResult {
     assert_clause_len(conclusion, 2)?;
+    assert_num_args(args, 1)?;
 
     let and_contents = match_term_err!((not (and ...)) = &conclusion[0])?;
-    if !and_contents.contains(&conclusion[1]) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::And,
-            conclusion[1].clone(),
-        ));
-    }
-    Ok(())
+
+    assert_eq(
+        &conclusion[1],
+        &and_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
+    )
 }
 
 pub fn and_neg(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
@@ -69,18 +68,17 @@ pub fn or_pos(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
     Ok(())
 }
 
-pub fn or_neg(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
+pub fn or_neg(RuleArgs { conclusion, args, .. }: RuleArgs) -> RuleResult {
     assert_clause_len(conclusion, 2)?;
+    assert_num_args(args, 1)?;
+
     let or_contents = match_term_err!((or ...) = &conclusion[0])?;
     let other = conclusion[1].remove_negation_err()?;
 
-    if !or_contents.contains(other) {
-        return Err(CheckerError::TermDoesntApperInOp(
-            Operator::Or,
-            other.clone(),
-        ));
-    }
-    Ok(())
+    assert_eq(
+        other,
+        &or_contents[args[0].as_integer().unwrap().to_usize().unwrap()],
+    )
 }
 
 pub fn xor_pos1(RuleArgs { conclusion, .. }: RuleArgs) -> RuleResult {
@@ -420,8 +418,8 @@ mod tests {
                 (declare-fun s () Bool)
             ",
             "Simple working examples" {
-                "(step t1 (cl (not (and p q r)) r) :rule and_pos)": true,
-                "(step t1 (cl (not (and (or (not r) p) q)) (or (not r) p)) :rule and_pos)": true,
+                "(step t1 (cl (not (and p q r)) r) :rule and_pos :args (2))": true,
+                "(step t1 (cl (not (and (or (not r) p) q)) (or (not r) p)) :rule and_pos :args (0))": true,
             }
             "First term in clause is not of the correct form" {
                 "(step t1 (cl (and p q r) r) :rule and_pos)": false,
@@ -502,7 +500,7 @@ mod tests {
                 (declare-fun s () Bool)
             ",
             "Simple working examples" {
-                "(step t1 (cl (or p q r) (not r)) :rule or_neg)": true,
+                "(step t1 (cl (or p q r) (not r)) :rule or_neg :args (2))": true,
             }
             "First term in clause is not of the correct form" {
                 "(step t1 (cl (and p q r) (not r)) :rule or_neg)": false,