From 8aaacd6d6e90643ebc383c9a7c16004820f32f66 Mon Sep 17 00:00:00 2001
From: David Doret <david.doret@me.com>
Date: Tue, 3 Oct 2023 21:47:44 +0200
Subject: [PATCH] documentation #195 + inference validation #126 + support for
 the composition of collection-like formulae + usage of
 sequent-collection-comma to define inference-rules + enhanced exceptions with
 user-friendly reports + #220 interdiction of variable-substitution of
 propositional objects with non-propositional objects.

---
 .idea/workspace.xml                    | 188 +++++++++++--------------
 src/punctilious/core.py                |  52 ++++---
 tests/test_conjunction_introduction.py |  20 +--
 3 files changed, 115 insertions(+), 145 deletions(-)

diff --git a/.idea/workspace.xml b/.idea/workspace.xml
index 73d292d5..6447b4c1 100644
--- a/.idea/workspace.xml
+++ b/.idea/workspace.xml
@@ -7,9 +7,7 @@
     <list default="true" id="48b609c4-0198-44a9-8f40-0a1e1f4ae31e" name="Changes" comment="documentation #195 + inference validation #126 + support for the composition of collection-like formulae + usage of sequent-collection-comma to define inference-rules + enhanced exceptions with user-friendly reports + #220 interdiction of variable-substitution of propositional objects with non-propositional objects.">
       <change beforePath="$PROJECT_DIR$/.idea/workspace.xml" beforeDir="false" afterPath="$PROJECT_DIR$/.idea/workspace.xml" afterDir="false" />
       <change beforePath="$PROJECT_DIR$/src/punctilious/core.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/punctilious/core.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_1.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_1.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_2.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_2.py" afterDir="false" />
-      <change beforePath="$PROJECT_DIR$/src/sample/sample_conjunction_introduction.py" beforeDir="false" afterPath="$PROJECT_DIR$/src/sample/sample_conjunction_introduction.py" afterDir="false" />
+      <change beforePath="$PROJECT_DIR$/tests/test_conjunction_introduction.py" beforeDir="false" afterPath="$PROJECT_DIR$/tests/test_conjunction_introduction.py" afterDir="false" />
     </list>
     <option name="SHOW_DIALOG" value="false" />
     <option name="HIGHLIGHT_CONFLICTS" value="true" />
@@ -122,7 +120,7 @@
       <recent name="C:\Users\David\PycharmProjects\punctilious\continuous_integration" />
     </key>
   </component>
-  <component name="RunManager" selected="Python.sample_conjunction_introduction">
+  <component name="RunManager" selected="Python tests.Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci">
     <configuration name="build" type="PythonConfigurationType" factoryName="Python" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
@@ -230,90 +228,6 @@
       <option name="INPUT_FILE" value="" />
       <method v="2" />
     </configuration>
-    <configuration name="sample_biconditional_introduction" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <envs>
-        <env name="PYTHONUNBUFFERED" value="1" />
-      </envs>
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_biconditional_introduction.py" />
-      <option name="PARAMETERS" value="" />
-      <option name="SHOW_COMMAND_LINE" value="false" />
-      <option name="EMULATE_TERMINAL" value="false" />
-      <option name="MODULE_MODE" value="false" />
-      <option name="REDIRECT_INPUT" value="false" />
-      <option name="INPUT_FILE" value="" />
-      <method v="2" />
-    </configuration>
-    <configuration name="sample_conjunction_elimination_1" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <envs>
-        <env name="PYTHONUNBUFFERED" value="1" />
-      </envs>
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_1.py" />
-      <option name="PARAMETERS" value="" />
-      <option name="SHOW_COMMAND_LINE" value="false" />
-      <option name="EMULATE_TERMINAL" value="false" />
-      <option name="MODULE_MODE" value="false" />
-      <option name="REDIRECT_INPUT" value="false" />
-      <option name="INPUT_FILE" value="" />
-      <method v="2" />
-    </configuration>
-    <configuration name="sample_conjunction_elimination_2" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <envs>
-        <env name="PYTHONUNBUFFERED" value="1" />
-      </envs>
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_conjunction_elimination_2.py" />
-      <option name="PARAMETERS" value="" />
-      <option name="SHOW_COMMAND_LINE" value="false" />
-      <option name="EMULATE_TERMINAL" value="false" />
-      <option name="MODULE_MODE" value="false" />
-      <option name="REDIRECT_INPUT" value="false" />
-      <option name="INPUT_FILE" value="" />
-      <method v="2" />
-    </configuration>
-    <configuration name="sample_conjunction_introduction" type="PythonConfigurationType" factoryName="Python" temporary="true" nameIsGenerated="true">
-      <module name="2023_05_02_PyCharmProject_Maths" />
-      <option name="INTERPRETER_OPTIONS" value="" />
-      <option name="PARENT_ENVS" value="true" />
-      <envs>
-        <env name="PYTHONUNBUFFERED" value="1" />
-      </envs>
-      <option name="SDK_HOME" value="" />
-      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/src/sample" />
-      <option name="IS_MODULE_SDK" value="true" />
-      <option name="ADD_CONTENT_ROOTS" value="true" />
-      <option name="ADD_SOURCE_ROOTS" value="true" />
-      <option name="SCRIPT_NAME" value="$PROJECT_DIR$/src/sample/sample_conjunction_introduction.py" />
-      <option name="PARAMETERS" value="" />
-      <option name="SHOW_COMMAND_LINE" value="false" />
-      <option name="EMULATE_TERMINAL" value="false" />
-      <option name="MODULE_MODE" value="false" />
-      <option name="REDIRECT_INPUT" value="false" />
-      <option name="INPUT_FILE" value="" />
-      <method v="2" />
-    </configuration>
     <configuration name="pytest tests" type="ShConfigurationType">
       <option name="SCRIPT_TEXT" value="pytest tests" />
       <option name="INDEPENDENT_SCRIPT_PATH" value="true" />
@@ -375,7 +289,49 @@
       <option name="docutils_open_in_browser" value="false" />
       <method v="2" />
     </configuration>
-    <configuration name="Python tests in test_axiom_interpretation.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+    <configuration name="Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="_new_additionalArguments" value="&quot;&quot;" />
+      <option name="_new_target" value="&quot;test_conjunction_introduction.TestConjunctionIntroduction.test_ci&quot;" />
+      <option name="_new_targetType" value="&quot;PYTHON&quot;" />
+      <method v="2" />
+    </configuration>
+    <configuration name="Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci_failure" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="_new_additionalArguments" value="&quot;&quot;" />
+      <option name="_new_target" value="&quot;test_conjunction_introduction.TestConjunctionIntroduction.test_ci_failure&quot;" />
+      <option name="_new_targetType" value="&quot;PYTHON&quot;" />
+      <method v="2" />
+    </configuration>
+    <configuration name="Python tests in test_conjunction_elimination_1.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="_new_additionalArguments" value="&quot;&quot;" />
+      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_conjunction_elimination_1.py&quot;" />
+      <option name="_new_targetType" value="&quot;PATH&quot;" />
+      <method v="2" />
+    </configuration>
+    <configuration name="Python tests in test_conjunction_elimination_2.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
       <module name="2023_05_02_PyCharmProject_Maths" />
       <option name="INTERPRETER_OPTIONS" value="" />
       <option name="PARENT_ENVS" value="true" />
@@ -385,7 +341,21 @@
       <option name="ADD_CONTENT_ROOTS" value="true" />
       <option name="ADD_SOURCE_ROOTS" value="true" />
       <option name="_new_additionalArguments" value="&quot;&quot;" />
-      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_axiom_interpretation.py&quot;" />
+      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_conjunction_elimination_2.py&quot;" />
+      <option name="_new_targetType" value="&quot;PATH&quot;" />
+      <method v="2" />
+    </configuration>
+    <configuration name="Python tests in test_conjunction_introduction.py" type="tests" factoryName="Autodetect" temporary="true" nameIsGenerated="true">
+      <module name="2023_05_02_PyCharmProject_Maths" />
+      <option name="INTERPRETER_OPTIONS" value="" />
+      <option name="PARENT_ENVS" value="true" />
+      <option name="SDK_HOME" value="" />
+      <option name="WORKING_DIRECTORY" value="$PROJECT_DIR$/tests" />
+      <option name="IS_MODULE_SDK" value="true" />
+      <option name="ADD_CONTENT_ROOTS" value="true" />
+      <option name="ADD_SOURCE_ROOTS" value="true" />
+      <option name="_new_additionalArguments" value="&quot;&quot;" />
+      <option name="_new_target" value="&quot;$PROJECT_DIR$/tests/test_conjunction_introduction.py&quot;" />
       <option name="_new_targetType" value="&quot;PATH&quot;" />
       <method v="2" />
     </configuration>
@@ -409,24 +379,24 @@
       <item itemvalue="Python.prebuild_generate_theory_reports" />
       <item itemvalue="Python.build" />
       <item itemvalue="Python.prebuild_generate_sample_outputs" />
-      <item itemvalue="Python.sample_biconditional_introduction" />
-      <item itemvalue="Python.sample_conjunction_elimination_1" />
-      <item itemvalue="Python.sample_conjunction_elimination_2" />
-      <item itemvalue="Python.sample_conjunction_introduction" />
       <item itemvalue="Python docs.Sphinx HTML" />
       <item itemvalue="Python tests.Python tests in tests" />
-      <item itemvalue="Python tests.Python tests in test_axiom_interpretation.py" />
+      <item itemvalue="Python tests.Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci" />
+      <item itemvalue="Python tests.Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci_failure" />
+      <item itemvalue="Python tests.Python tests in test_conjunction_elimination_1.py" />
+      <item itemvalue="Python tests.Python tests in test_conjunction_elimination_2.py" />
+      <item itemvalue="Python tests.Python tests in test_conjunction_introduction.py" />
       <item itemvalue="Shell Script.pytest tests" />
       <item itemvalue="Shell Script.pytest" />
       <item itemvalue="Shell Script.python -m build" />
     </list>
     <recent_temporary>
       <list>
-        <item itemvalue="Python.sample_conjunction_introduction" />
-        <item itemvalue="Python.sample_conjunction_elimination_2" />
-        <item itemvalue="Python.sample_conjunction_elimination_1" />
-        <item itemvalue="Python.sample_biconditional_introduction" />
-        <item itemvalue="Python tests.Python tests in test_axiom_interpretation.py" />
+        <item itemvalue="Python tests.Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci" />
+        <item itemvalue="Python tests.Python tests for test_conjunction_introduction.TestConjunctionIntroduction.test_ci_failure" />
+        <item itemvalue="Python tests.Python tests in test_conjunction_introduction.py" />
+        <item itemvalue="Python tests.Python tests in test_conjunction_elimination_2.py" />
+        <item itemvalue="Python tests.Python tests in test_conjunction_elimination_1.py" />
       </list>
     </recent_temporary>
   </component>
@@ -439,14 +409,6 @@
       <option name="presentableId" value="Default" />
       <updated>1687980987309</updated>
     </task>
-    <task id="LOCAL-00289" summary="#201 + #195">
-      <option name="closed" value="true" />
-      <created>1694932915854</created>
-      <option name="number" value="00289" />
-      <option name="presentableId" value="LOCAL-00289" />
-      <option name="project" value="LOCAL" />
-      <updated>1694932915854</updated>
-    </task>
     <task id="LOCAL-00290" summary="#201 + #195">
       <option name="closed" value="true" />
       <created>1694933881746</created>
@@ -831,7 +793,15 @@
       <option name="project" value="LOCAL" />
       <updated>1696331518332</updated>
     </task>
-    <option name="localTasksCounter" value="338" />
+    <task id="LOCAL-00338" summary="documentation #195 + inference validation #126 + support for the composition of collection-like formulae + usage of sequent-collection-comma to define inference-rules + enhanced exceptions with user-friendly reports + #220 interdiction of variable-substitution of propositional objects with non-propositional objects.">
+      <option name="closed" value="true" />
+      <created>1696332797135</created>
+      <option name="number" value="00338" />
+      <option name="presentableId" value="LOCAL-00338" />
+      <option name="project" value="LOCAL" />
+      <updated>1696332797135</updated>
+    </task>
+    <option name="localTasksCounter" value="339" />
     <servers />
   </component>
   <component name="Vcs.Log.Tabs.Properties">
diff --git a/src/punctilious/core.py b/src/punctilious/core.py
index 7ac67286..41adc965 100644
--- a/src/punctilious/core.py
+++ b/src/punctilious/core.py
@@ -3427,8 +3427,7 @@ def i(self):
     def inference_rule(self):
         return self._inference_rule
 
-    def verify_compatibility(self, *args):
-        return self.inference_rule.check_inference_validity(*args, t=self.theory)
+    # def verify_compatibility(self, *args):  #    return self.inference_rule.check_inference_validity(*args, t=self.theory)
 
 
 class DefinitionDeclaration(TheoreticalObject):
@@ -4149,8 +4148,11 @@ def construct_formula(self, p_and_q: FlexibleFormula) -> Formula:
         .. include:: ../../include/construct_formula_python_method.rstinc
 
         """
+        error_code: ErrorCode = error_codes.error_002_inference_premise_syntax_error
         _, p_and_q, _ = verify_formula(arg='p_and_q', input_value=p_and_q, u=self.u,
-            form=self.parameter_p_and_q, mask=self.parameter_p_and_q_mask, raise_exception=True)
+            form=self.parameter_p_and_q, mask=self.parameter_p_and_q_mask, raise_exception=True,
+            error_code=error_code)
+        p_and_q: Formula
         p: Formula = p_and_q.parameters[0]
         output: Formula = p
         return output
@@ -4192,8 +4194,11 @@ def construct_formula(self, p_and_q: FlexibleFormula) -> Formula:
         .. include:: ../../include/construct_formula_python_method.rstinc
 
         """
+        error_code: ErrorCode = error_codes.error_002_inference_premise_syntax_error
         _, p_and_q, _ = verify_formula(arg='p_and_q', input_value=p_and_q, u=self.u,
-            form=self.parameter_p_and_q, mask=self.parameter_p_and_q_mask, raise_exception=True)
+            form=self.parameter_p_and_q, mask=self.parameter_p_and_q_mask, raise_exception=True,
+            error_code=error_code)
+        p_and_q: Formula
         q: Formula = p_and_q.parameters[1]
         output: Formula = q
         return output
@@ -4217,7 +4222,7 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'conjunction introduction inference rule'
         name = 'conjunction introduction'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q:
-            definition = ((p | u.r.sequent_premises | q) | u.r.proves | (p | u.r.land | q))
+            definition = u.r.sequent_premises(p, q) | u.r.proves | (p | u.r.land | q)
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
@@ -4227,9 +4232,15 @@ def construct_formula(self, p: FlexibleFormula, q: FlexibleFormula) -> Formula:
         .. include:: ../../include/construct_formula_python_method.rstinc
 
         """
-        _, p, _ = verify_formula(arg='p', input_value=p, u=self.u, raise_exception=True)
-        _, q, _ = verify_formula(arg='q', input_value=q, u=self.u, raise_exception=True)
+        error_code: ErrorCode = error_codes.error_002_inference_premise_syntax_error
+        _, p, _ = verify_formula(arg='p', input_value=p, u=self.u, raise_exception=True,
+            error_code=error_code)
+        p: Formula
+        _, q, _ = verify_formula(arg='q', input_value=q, u=self.u, raise_exception=True,
+            error_code=error_code)
+        q: Formula
         output: Formula = p | self.u.r.land | q
+        return output
 
 
 class ConstructiveDilemmaDeclaration(InferenceRuleDeclaration):
@@ -4253,23 +4264,29 @@ def __init__(self, universe_of_discourse: UniverseOfDiscourse, echo: (None, bool
         explicit_name = 'constructive dilemma inference rule'
         name = 'constructive dilemma'
         with u.v(symbol='P') as p, u.v(symbol='Q') as q, u.v(symbol='R') as r, u.v(symbol='S') as s:
-            # TODO: FEATURE #216: Review this definition once sequence-comma supports n-ary components.
-            definition = ((p | u.r.implies | q) | u.r.sequent_premises | (
-                    (r | u.r.implies | s) | u.r.sequent_premises | (
-                    p | u.r.lor | r))) | u.r.proves | (q | u.r.lor | s)
+            definition = u.r.sequent_premises((p | u.r.implies | q), (r | u.r.implies | s),
+                (p | u.r.lor | r)) | u.r.proves | (q | u.r.lor | s)
+        with u.v(symbol='P') as p, u.v(symbol='Q') as q:
+            self.parameter_p_implies_q = p | u.r.implies | q
+            self.parameter_p_implies_q_mask = frozenset([p, q])
+        with u.v(symbol='R') as r, u.v(symbol='S') as s:
+            self.parameter_r_implies_s = r | u.r.implies | s
+            self.parameter_r_implies_s_mask = frozenset([r, s])
+        with u.v(symbol='P') as p, u.v(symbol='R') as r:
+            self.parameter_p_or_r = p | u.r.lor | r
+            self.parameter_p_or_r_mask = frozenset([p, r])
         super().__init__(definition=definition, universe_of_discourse=universe_of_discourse,
             symbol=symbol, auto_index=auto_index, dashed_name=dashed_name, acronym=acronym,
             abridged_name=abridged_name, name=name, explicit_name=explicit_name, echo=echo)
 
-    def infer_formula(self, p_implies_q: FormulaStatement, r_implies_s: FormulaStatement,
-            p_or_r: FormulaStatement, t: TheoryElaborationSequence,
-            echo: (None, bool) = None) -> Formula:
+    def infer_formula(self, p_implies_q: FlexibleFormula, r_implies_s: FlexibleFormula,
+            p_or_r: FlexibleFormula) -> Formula:
         """
         .. include:: ../../include/construct_formula_python_method.rstinc
 
         """
-        _, p_implies_q, _ = verify_formula(u=t.u, arity=None, input_value=p_implies_q)
-        _, r_implies_s, _ = verify_formula(u=t.u, arity=None, input_value=r_implies_s)
+        _, p_implies_q, _ = verify_formula(u=t.u, input_value=p_implies_q, )
+        _, r_implies_s, _ = verify_formula(u=t.u, input_value=r_implies_s)
         _, p_or_r, _ = verify_formula(u=t.u, arity=None, input_value=p_or_r)
         return p | t.u.r.land | q
 
@@ -7136,8 +7153,7 @@ def construct_formula(self, p_and_q: FlexibleFormula) -> Formula:
         """
         return self.i.construct_formula(p_and_q=p_and_q)
 
-    def infer_formula_statement(self, p_and_q: FlexibleFormula,
-            nameset: (None, str, NameSet) = None, ref: (None, str) = None,
+    def infer_formula_statement(self, p_and_q: FlexibleFormula, ref: (None, str) = None,
             paragraph_header: (None, ParagraphHeader) = None, subtitle: (None, str) = None,
             echo: (None, bool) = None) -> InferredStatement:
         """
diff --git a/tests/test_conjunction_introduction.py b/tests/test_conjunction_introduction.py
index ca6ae998..0851da61 100644
--- a/tests/test_conjunction_introduction.py
+++ b/tests/test_conjunction_introduction.py
@@ -7,6 +7,7 @@ class TestConjunctionIntroduction(TestCase):
     def test_ci(self):
         import sample.sample_conjunction_introduction as test
         u: pu.UniverseOfDiscourse = test.u
+        t1: pu.TheoryElaborationSequence = test.t1
         o1: pu.SimpleObjct = test.o1
         o2: pu.SimpleObjct = test.o2
         o3: pu.SimpleObjct = test.o3
@@ -19,23 +20,6 @@ def test_ci(self):
             proposition_of_interest.rep_formula(pu.encodings.plaintext))
         self.assertEqual('(𝑟₁(𝑜₁, 𝑜₂) ∧ 𝑟₂(𝑜₃))',
             proposition_of_interest.rep_formula(pu.encodings.unicode))
-
-    def test_ci_failure(self):
-        pu.configuration.echo_default = True
-        u = pu.UniverseOfDiscourse()
-        o1 = u.o.declare()
-        o2 = u.o.declare()
-        o3 = u.o.declare()
-        r1 = u.r.declare(2, signal_proposition=True)
-        r2 = u.r.declare(1, signal_proposition=True)
-        t = u.t()
-        a = u.declare_axiom(random_data.random_sentence())
-        ap = t.include_axiom(a)
-        t.i.axiom_interpretation.infer_formula_statement(ap, r1(o1, o2))
-        t.i.axiom_interpretation.infer_formula_statement(ap, r2(o3))
-        phi3 = t.i.ci.infer_formula_statement(p=r1(o1, o2), q=r2(o3))
-        self.assertTrue(phi3.is_formula_syntactically_equivalent_to(r1(o1, o2) | u.r.land | r2(o3)))
-        self.assertEqual('(𝑟₁(𝑜₁, 𝑜₂) ∧ 𝑟₂(𝑜₃))', phi3.rep_formula(encoding=pu.encodings.unicode))
         # Trying to pass a formula that is not a valid formula-statement must raise an Exception
         with self.assertRaises(pu.PunctiliousException):
-            phi4 = t.i.ci.infer_formula_statement(p=r1(o1, o2), q=r1(o1, o3))
+            t1.i.conjunction_introduction.infer_formula_statement(p=r1(o1, o2), q=r1(o1, o3))