diff --git a/src/aba/mod.rs b/src/aba/mod.rs
index 0b252a8..3be747f 100644
--- a/src/aba/mod.rs
+++ b/src/aba/mod.rs
@@ -88,6 +88,10 @@ impl<A: Atom> Aba<A> {
     fn has_assumption(&self, atom: &A) -> bool {
         self.inverses.contains_key(atom)
     }
+
+    fn has_element(&self, element: &A) -> bool {
+        self.universe().any(|e| element == e)
+    }
 }
 
 fn body_to_clauses<I: TheoryAtom<A>, A: Atom>(head: Literal, body: &HashSet<A>) -> ClauseList {
diff --git a/src/aba/problems/admissibility.rs b/src/aba/problems/admissibility.rs
index f8f39d9..b31480b 100644
--- a/src/aba/problems/admissibility.rs
+++ b/src/aba/problems/admissibility.rs
@@ -29,7 +29,7 @@ pub struct VerifyAdmissibleExtension<A: Atom> {
 
 /// Decide whether `assumption` is credulously admissible in an [`Aba`]
 pub struct DecideCredulousAdmissibility<A> {
-    pub assumption: A,
+    pub element: A,
 }
 
 pub fn initial_admissibility_clauses<I: TheoryAtom<A>, A: Atom>(aba: &Aba<A>) -> ClauseList {
@@ -222,7 +222,7 @@ impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
 
     fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
         let mut clauses = initial_admissibility_clauses::<SetTheory<_>, _>(aba);
-        clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
+        clauses.push(Clause::from(vec![SetTheory(self.element.clone()).pos()]));
         clauses
     }
 
@@ -231,12 +231,12 @@ impl<A: Atom> Problem<A> for DecideCredulousAdmissibility<A> {
     }
 
     fn check(&self, aba: &Aba<A>) -> Result {
-        if aba.has_assumption(&self.assumption) {
+        if aba.has_assumption(&self.element) {
             Ok(())
         } else {
             Err(Error::ProblemCheckFailed(format!(
                 "Assumption {:?} not present in ABA framework",
-                self.assumption
+                self.element
             )))
         }
     }
diff --git a/src/aba/problems/complete.rs b/src/aba/problems/complete.rs
index 1259468..d51bb0b 100644
--- a/src/aba/problems/complete.rs
+++ b/src/aba/problems/complete.rs
@@ -20,7 +20,7 @@ pub struct EnumerateCompleteExtensions<A> {
 
 /// Decide whether `assumption` is credulously complete in an [`Aba`]
 pub struct DecideCredulousComplete<A> {
-    pub assumption: A,
+    pub element: A,
 }
 
 fn initial_complete_clauses<A: Atom>(aba: &Aba<A>) -> ClauseList {
@@ -101,7 +101,7 @@ impl<A: Atom> Problem<A> for DecideCredulousComplete<A> {
 
     fn additional_clauses(&self, aba: &Aba<A>) -> ClauseList {
         let mut clauses = initial_complete_clauses(aba);
-        clauses.push(Clause::from(vec![SetTheory(self.assumption.clone()).pos()]));
+        clauses.push(Clause::from(vec![SetTheory(self.element.clone()).pos()]));
         clauses
     }
 
@@ -110,12 +110,12 @@ impl<A: Atom> Problem<A> for DecideCredulousComplete<A> {
     }
 
     fn check(&self, aba: &Aba<A>) -> Result {
-        if aba.has_assumption(&self.assumption) {
+        if aba.has_element(&self.element) {
             Ok(())
         } else {
             Err(Error::ProblemCheckFailed(format!(
-                "Assumption {:?} not present in ABA framework",
-                self.assumption
+                "Element {:?} not present in ABA framework",
+                self.element
             )))
         }
     }
diff --git a/src/main.rs b/src/main.rs
index fa553c2..96cb6c6 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -64,15 +64,14 @@ fn __main() -> Result {
             aba::problems::solve(SampleAdmissibleExtension, &aba)?.fmt_iccma()
         }
         args::Problems::DecideCredulousAdmissibility { query } => {
-            aba::problems::solve(DecideCredulousAdmissibility { assumption: query }, &aba)?
-                .fmt_iccma()
+            aba::problems::solve(DecideCredulousAdmissibility { element: query }, &aba)?.fmt_iccma()
         }
         args::Problems::EnumerateComplete => {
             aba::problems::multishot_solve(EnumerateCompleteExtensions::default(), &aba)?
                 .fmt_iccma()
         }
         args::Problems::DecideCredulousComplete { query } => {
-            aba::problems::solve(DecideCredulousComplete { assumption: query }, &aba)?.fmt_iccma()
+            aba::problems::solve(DecideCredulousComplete { element: query }, &aba)?.fmt_iccma()
         }
     }?;
     let mut stdout = std::io::stdout().lock();