import unittest

from logics.classes.propositional import Inference, Formula
from logics.classes.propositional.proof_theories import NaturalDeductionStep, NaturalDeductionRule
from logics.utils.parsers import classical_parser
from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system


class TestClassicalNaturalDeductionSystem(unittest.TestCase):
    def test_natural_deduction_rule(self):
        """Test overriding of index and len methods in NaturalDeductionRule"""
        rule = NaturalDeductionRule([
            '(...)',
            NaturalDeductionStep(Formula(['→', ['A'], ['B']])),
            '(...)',
            NaturalDeductionStep(Formula(['B']), 'E→', [0, 1])
        ])
        self.assertEqual(rule.index(NaturalDeductionStep(Formula(['B']), 'E→', [0, 1])), 1)
        self.assertEqual(len(rule), 2)

    def test_nd_system(self):
        """Test the method that tells if a step is a correct application of a rule"""

        # A correct derivation
        deriv = classical_parser.parse_derivation(
            """p; premise
            (p → q); premise
            q; E→; [1, 0]; []
            p ∧ q; I∧; [0, 2]; []""",
            natural_deduction=True)

        # Check is application of the correct rule, and a different rule
        self.assertTrue(nd_system.is_correct_application(deriv, 2, nd_system.rules['E→']))
        self.assertFalse(nd_system.is_correct_application(deriv, 2, nd_system.rules['E∧2']))
        self.assertTrue(nd_system.is_correct_application(deriv, 3, nd_system.rules['I∧']))
        self.assertFalse(nd_system.is_correct_application(deriv, 3, nd_system.rules['E→']))

        # Check is correct derivation of the correct and an incorrect inference
        i = Inference([Formula(['p']), Formula(['→', ['p'], ['q']])],
                      [Formula(['∧', ['p'], ['q']])])
        self.assertTrue(nd_system.is_correct_derivation(deriv, i))
        i2 = Inference([Formula(['p']), Formula(['→', ['p'], ['q']])],
                      [Formula(['∧', ['q'], ['p']])])
        self.assertFalse(nd_system.is_correct_derivation(deriv, i2))

        # Repeating steps should not alter the outcome (should print a warning)
        # deriv2_0 = classical_parser.parse_derivation(
        #     """p; supposition; []; [0]
        #     p; repetition; [0, 0]; [0]""",
        #     natural_deduction=True)
        # self.assertTrue(nd_system.is_correct_application(deriv2_0, 1, nd_system.rules['repetition']))

        # Test step in the future
        deriv2_1 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [1]; [0]""",
            natural_deduction=True)
        deriv2_2 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [2]; [0]""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv2_1, 1, nd_system.rules['repetition']))
        self.assertFalse(nd_system.is_correct_application(deriv2_2, 1, nd_system.rules['repetition']))

        # -------------------------------------------------
        # Test incorrect use of suppositions

        # Using a step in a closed supposition
        deriv3_1 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [0]; [0]
            (p → p); I→; [0, 1]; []
            p; E→; [2, 0]; []""",
            natural_deduction=True)
        # Check correct application of rep and I→
        self.assertTrue(nd_system.is_correct_application(deriv3_1, 1, nd_system.rules['repetition']))
        self.assertTrue(nd_system.is_correct_application(deriv3_1, 2, nd_system.rules['I→']))
        self.assertFalse(nd_system.is_correct_application(deriv3_1, 3, nd_system.rules['E→']))

        # Closing a supposition with a rule that does not close
        deriv3_2 = classical_parser.parse_derivation('''
            p; premise
            p; supposition; []; [1]
            p; repetition; [0]; [1]
            (p ∨ q); I∨1; [0]; []''',
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv3_2, 3, nd_system.rules['I∨1']))

        # Closing two suppositions at once
        deriv3_3 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; supposition; [0]; [0, 1]
            (p → p); I→; [0, 1]; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv3_3, 2, nd_system.rules['I→']))

        # Not closing a supposition with a rule that does close
        deriv3_4 = classical_parser.parse_derivation(
            """p; supposition; []; [0]
            p; repetition; [0]; [0]
            (p → p); I→; [0, 1]; [0]""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_application(deriv3_4, 2, nd_system.rules['I→']))

        # Incorrect opening of suppositions
        deriv3_5 = classical_parser.parse_derivation(
            """p; supposition; []; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv3_5, None))
        deriv3_6 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; supposition; []; [0]""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv3_6, None))

        # -------------------------------------------------
        # A correct derivation using all the rules

        deriv4 = classical_parser.parse_derivation(
            """q; premise; []; []
            ~q; supposition; []; [1]
            ~q; repetition; [1]; [1]
            (q ∧ ~q); I∧; [0, 2]; [1]
            q; E∧1; [3]; [1]
            ⊥; E~; [1, 4]; [1]
            p; EFSQ; [5]; [1]
            ⊥; repetition; [5]; [1]
            ~~q; I~; [1, 7]; []
            q; ~~; [8]; []
            q; supposition; []; [10]
            q; repetition; [10]; [10]
            (q → q); I→; [10, 11]; []
            q; E→; [12, 9]; []
            (q ∨ p); I∨1; [13]; []
            (p → q); premise; []; []
            q; E∨; [14, 12, 15]; []
            """, natural_deduction=True)
        i3 = Inference([Formula(['q']), Formula(['→', ['p'], ['q']])],
                       [Formula(['q'])])
        self.assertTrue(nd_system.is_correct_derivation(deriv4, i3))

    def test_rule_order(self):
        # i1 is conjunction introduction
        i1 = Inference([Formula(['p']), Formula(['q'])],
                      [Formula(['∧', ['p'], ['q']])])

        # First derivation: standard one
        deriv1_1 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (p ∧ q); I∧; [0, 1]; []""",
            natural_deduction=True)
        self.assertTrue(nd_system.is_correct_derivation(deriv1_1, i1))

        # Second derivation: reverse on_steps order
        deriv1_2 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (p ∧ q); I∧; [1, 0]; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv1_2, i1))

        i2 = Inference([Formula(['p']), Formula(['q'])],
                       [Formula(['∧', ['q'], ['p']])])

        # Third derivation: reverse the conjuncts
        deriv2_1 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (q ∧ p); I∧; [1, 0]; []""",
            natural_deduction=True)
        self.assertTrue(nd_system.is_correct_derivation(deriv2_1, i2))

        # Fourth derivation: reverse the conjuncts and the on_steps
        deriv2_2 = classical_parser.parse_derivation(
            """p; premise; []; []
            q; premise; []; []
            (q ∧ p); I∧; [0, 1]; []""",
            natural_deduction=True)
        self.assertFalse(nd_system.is_correct_derivation(deriv2_2, i2))


if __name__ == '__main__':
    unittest.main()

[((7981, 7996), 'unittest.main', 'unittest.main', ([], {}), '()\n', (7994, 7996), False, 'import unittest\n'), ((1035, 1213), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; premise\n            (p → q); premise\n            q; E→; [1, 0]; []\n            p ∧ q; I∧; [0, 2]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; premise\n            (p → q); premise\n            q; E→; [1, 0]; []\n            p ∧ q; I∧; [0, 2]; []"""\n    , natural_deduction=True)\n', (1068, 1213), False, 'from logics.utils.parsers import classical_parser\n'), ((2555, 2688), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; supposition; []; [0]\n            p; repetition; [1]; [0]"""'], {'natural_deduction': '(True)'}), '(\n    """p; supposition; []; [0]\n            p; repetition; [1]; [0]""",\n    natural_deduction=True)\n', (2588, 2688), False, 'from logics.utils.parsers import classical_parser\n'), ((2724, 2857), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; supposition; []; [0]\n            p; repetition; [2]; [0]"""'], {'natural_deduction': '(True)'}), '(\n    """p; supposition; []; [0]\n            p; repetition; [2]; [0]""",\n    natural_deduction=True)\n', (2757, 2857), False, 'from logics.utils.parsers import classical_parser\n'), ((3253, 3453), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; supposition; []; [0]\n            p; repetition; [0]; [0]\n            (p → p); I→; [0, 1]; []\n            p; E→; [2, 0]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; supposition; []; [0]\n            p; repetition; [0]; [0]\n            (p → p); I→; [0, 1]; []\n            p; E→; [2, 0]; []"""\n    , natural_deduction=True)\n', (3286, 3453), False, 'from logics.utils.parsers import classical_parser\n'), ((3894, 4098), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""\n            p; premise\n            p; supposition; []; [1]\n            p; repetition; [0]; [1]\n            (p ∨ q); I∨1; [0]; []"""'], {'natural_deduction': '(True)'}), '(\n    """\n            p; premise\n            p; supposition; []; [1]\n            p; repetition; [0]; [1]\n            (p ∨ q); I∨1; [0]; []"""\n    , natural_deduction=True)\n', (3927, 4098), False, 'from logics.utils.parsers import classical_parser\n'), ((4260, 4434), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; supposition; []; [0]\n            p; supposition; [0]; [0, 1]\n            (p → p); I→; [0, 1]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; supposition; []; [0]\n            p; supposition; [0]; [0, 1]\n            (p → p); I→; [0, 1]; []"""\n    , natural_deduction=True)\n', (4293, 4434), False, 'from logics.utils.parsers import classical_parser\n'), ((4629, 4800), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; supposition; []; [0]\n            p; repetition; [0]; [0]\n            (p → p); I→; [0, 1]; [0]"""'], {'natural_deduction': '(True)'}), '(\n    """p; supposition; []; [0]\n            p; repetition; [0]; [0]\n            (p → p); I→; [0, 1]; [0]"""\n    , natural_deduction=True)\n', (4662, 4800), False, 'from logics.utils.parsers import classical_parser\n'), ((4975, 5062), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; supposition; []; []"""'], {'natural_deduction': '(True)'}), "('p; supposition; []; []',\n    natural_deduction=True)\n", (5008, 5062), False, 'from logics.utils.parsers import classical_parser\n'), ((5181, 5309), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; premise; []; []\n            q; supposition; []; [0]"""'], {'natural_deduction': '(True)'}), '(\n    """p; premise; []; []\n            q; supposition; []; [0]""",\n    natural_deduction=True)\n', (5214, 5309), False, 'from logics.utils.parsers import classical_parser\n'), ((5530, 6185), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""q; premise; []; []\n            ~q; supposition; []; [1]\n            ~q; repetition; [1]; [1]\n            (q ∧ ~q); I∧; [0, 2]; [1]\n            q; E∧1; [3]; [1]\n            ⊥; E~; [1, 4]; [1]\n            p; EFSQ; [5]; [1]\n            ⊥; repetition; [5]; [1]\n            ~~q; I~; [1, 7]; []\n            q; ~~; [8]; []\n            q; supposition; []; [10]\n            q; repetition; [10]; [10]\n            (q → q); I→; [10, 11]; []\n            q; E→; [12, 9]; []\n            (q ∨ p); I∨1; [13]; []\n            (p → q); premise; []; []\n            q; E∨; [14, 12, 15]; []\n            """'], {'natural_deduction': '(True)'}), '(\n    """q; premise; []; []\n            ~q; supposition; []; [1]\n            ~q; repetition; [1]; [1]\n            (q ∧ ~q); I∧; [0, 2]; [1]\n            q; E∧1; [3]; [1]\n            ⊥; E~; [1, 4]; [1]\n            p; EFSQ; [5]; [1]\n            ⊥; repetition; [5]; [1]\n            ~~q; I~; [1, 7]; []\n            q; ~~; [8]; []\n            q; supposition; []; [10]\n            q; repetition; [10]; [10]\n            (q → q); I→; [10, 11]; []\n            q; E→; [12, 9]; []\n            (q ∨ p); I∨1; [13]; []\n            (p → q); premise; []; []\n            q; E∨; [14, 12, 15]; []\n            """\n    , natural_deduction=True)\n', (5563, 6185), False, 'from logics.utils.parsers import classical_parser\n'), ((6615, 6775), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; premise; []; []\n            q; premise; []; []\n            (p ∧ q); I∧; [0, 1]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; premise; []; []\n            q; premise; []; []\n            (p ∧ q); I∧; [0, 1]; []"""\n    , natural_deduction=True)\n', (6648, 6775), False, 'from logics.utils.parsers import classical_parser\n'), ((6934, 7094), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; premise; []; []\n            q; premise; []; []\n            (p ∧ q); I∧; [1, 0]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; premise; []; []\n            q; premise; []; []\n            (p ∧ q); I∧; [1, 0]; []"""\n    , natural_deduction=True)\n', (6967, 7094), False, 'from logics.utils.parsers import classical_parser\n'), ((7365, 7525), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; premise; []; []\n            q; premise; []; []\n            (q ∧ p); I∧; [1, 0]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; premise; []; []\n            q; premise; []; []\n            (q ∧ p); I∧; [1, 0]; []"""\n    , natural_deduction=True)\n', (7398, 7525), False, 'from logics.utils.parsers import classical_parser\n'), ((7700, 7860), 'logics.utils.parsers.classical_parser.parse_derivation', 'classical_parser.parse_derivation', (['"""p; premise; []; []\n            q; premise; []; []\n            (q ∧ p); I∧; [0, 1]; []"""'], {'natural_deduction': '(True)'}), '(\n    """p; premise; []; []\n            q; premise; []; []\n            (q ∧ p); I∧; [0, 1]; []"""\n    , natural_deduction=True)\n', (7733, 7860), False, 'from logics.utils.parsers import classical_parser\n'), ((1327, 1392), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv', '(2)', "nd_system.rules['E→']"], {}), "(deriv, 2, nd_system.rules['E→'])\n", (1359, 1392), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((1419, 1485), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv', '(2)', "nd_system.rules['E∧2']"], {}), "(deriv, 2, nd_system.rules['E∧2'])\n", (1451, 1485), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((1511, 1576), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv', '(3)', "nd_system.rules['I∧']"], {}), "(deriv, 3, nd_system.rules['I∧'])\n", (1543, 1576), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((1603, 1668), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv', '(3)', "nd_system.rules['E→']"], {}), "(deriv, 3, nd_system.rules['E→'])\n", (1635, 1668), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((1899, 1940), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv', 'i'], {}), '(deriv, i)\n', (1930, 1940), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((2092, 2134), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv', 'i2'], {}), '(deriv, i2)\n', (2123, 2134), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((2899, 2975), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv2_1', '(1)', "nd_system.rules['repetition']"], {}), "(deriv2_1, 1, nd_system.rules['repetition'])\n", (2931, 2975), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((3002, 3078), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv2_2', '(1)', "nd_system.rules['repetition']"], {}), "(deriv2_2, 1, nd_system.rules['repetition'])\n", (3034, 3078), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((3543, 3619), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv3_1', '(1)', "nd_system.rules['repetition']"], {}), "(deriv3_1, 1, nd_system.rules['repetition'])\n", (3575, 3619), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((3645, 3713), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv3_1', '(2)', "nd_system.rules['I→']"], {}), "(deriv3_1, 2, nd_system.rules['I→'])\n", (3677, 3713), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((3740, 3808), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv3_1', '(3)', "nd_system.rules['E→']"], {}), "(deriv3_1, 3, nd_system.rules['E→'])\n", (3772, 3808), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((4126, 4195), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv3_2', '(3)', "nd_system.rules['I∨1']"], {}), "(deriv3_2, 3, nd_system.rules['I∨1'])\n", (4158, 4195), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((4475, 4543), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv3_3', '(2)', "nd_system.rules['I→']"], {}), "(deriv3_3, 2, nd_system.rules['I→'])\n", (4507, 4543), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((4841, 4909), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_application', 'nd_system.is_correct_application', (['deriv3_4', '(2)', "nd_system.rules['I→']"], {}), "(deriv3_4, 2, nd_system.rules['I→'])\n", (4873, 4909), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((5113, 5160), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv3_5', 'None'], {}), '(deriv3_5, None)\n', (5144, 5160), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((5351, 5398), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv3_6', 'None'], {}), '(deriv3_6, None)\n', (5382, 5398), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((6325, 6368), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv4', 'i3'], {}), '(deriv4, i3)\n', (6356, 6368), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((6815, 6860), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv1_1', 'i1'], {}), '(deriv1_1, i1)\n', (6846, 6860), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((7135, 7180), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv1_2', 'i1'], {}), '(deriv1_2, i1)\n', (7166, 7180), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((7565, 7610), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv2_1', 'i2'], {}), '(deriv2_1, i2)\n', (7596, 7610), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((7901, 7946), 'logics.instances.propositional.natural_deduction.classical_natural_deduction_system.is_correct_derivation', 'nd_system.is_correct_derivation', (['deriv2_2', 'i2'], {}), '(deriv2_2, i2)\n', (7932, 7946), True, 'from logics.instances.propositional.natural_deduction import classical_natural_deduction_system as nd_system\n'), ((1774, 1788), 'logics.classes.propositional.Formula', 'Formula', (["['p']"], {}), "(['p'])\n", (1781, 1788), False, 'from logics.classes.propositional import Inference, Formula\n'), ((1790, 1818), 'logics.classes.propositional.Formula', 'Formula', (["['→', ['p'], ['q']]"], {}), "(['→', ['p'], ['q']])\n", (1797, 1818), False, 'from logics.classes.propositional import Inference, Formula\n'), ((1844, 1872), 'logics.classes.propositional.Formula', 'Formula', (["['∧', ['p'], ['q']]"], {}), "(['∧', ['p'], ['q']])\n", (1851, 1872), False, 'from logics.classes.propositional import Inference, Formula\n'), ((1966, 1980), 'logics.classes.propositional.Formula', 'Formula', (["['p']"], {}), "(['p'])\n", (1973, 1980), False, 'from logics.classes.propositional import Inference, Formula\n'), ((1982, 2010), 'logics.classes.propositional.Formula', 'Formula', (["['→', ['p'], ['q']]"], {}), "(['→', ['p'], ['q']])\n", (1989, 2010), False, 'from logics.classes.propositional import Inference, Formula\n'), ((2036, 2064), 'logics.classes.propositional.Formula', 'Formula', (["['∧', ['q'], ['p']]"], {}), "(['∧', ['q'], ['p']])\n", (2043, 2064), False, 'from logics.classes.propositional import Inference, Formula\n'), ((6213, 6227), 'logics.classes.propositional.Formula', 'Formula', (["['q']"], {}), "(['q'])\n", (6220, 6227), False, 'from logics.classes.propositional import Inference, Formula\n'), ((6229, 6257), 'logics.classes.propositional.Formula', 'Formula', (["['→', ['p'], ['q']]"], {}), "(['→', ['p'], ['q']])\n", (6236, 6257), False, 'from logics.classes.propositional import Inference, Formula\n'), ((6284, 6298), 'logics.classes.propositional.Formula', 'Formula', (["['q']"], {}), "(['q'])\n", (6291, 6298), False, 'from logics.classes.propositional import Inference, Formula\n'), ((6467, 6481), 'logics.classes.propositional.Formula', 'Formula', (["['p']"], {}), "(['p'])\n", (6474, 6481), False, 'from logics.classes.propositional import Inference, Formula\n'), ((6483, 6497), 'logics.classes.propositional.Formula', 'Formula', (["['q']"], {}), "(['q'])\n", (6490, 6497), False, 'from logics.classes.propositional import Inference, Formula\n'), ((6523, 6551), 'logics.classes.propositional.Formula', 'Formula', (["['∧', ['p'], ['q']]"], {}), "(['∧', ['p'], ['q']])\n", (6530, 6551), False, 'from logics.classes.propositional import Inference, Formula\n'), ((7207, 7221), 'logics.classes.propositional.Formula', 'Formula', (["['p']"], {}), "(['p'])\n", (7214, 7221), False, 'from logics.classes.propositional import Inference, Formula\n'), ((7223, 7237), 'logics.classes.propositional.Formula', 'Formula', (["['q']"], {}), "(['q'])\n", (7230, 7237), False, 'from logics.classes.propositional import Inference, Formula\n'), ((7264, 7292), 'logics.classes.propositional.Formula', 'Formula', (["['∧', ['q'], ['p']]"], {}), "(['∧', ['q'], ['p']])\n", (7271, 7292), False, 'from logics.classes.propositional import Inference, Formula\n'), ((613, 641), 'logics.classes.propositional.Formula', 'Formula', (["['→', ['A'], ['B']]"], {}), "(['→', ['A'], ['B']])\n", (620, 641), False, 'from logics.classes.propositional import Inference, Formula\n'), ((698, 712), 'logics.classes.propositional.Formula', 'Formula', (["['B']"], {}), "(['B'])\n", (705, 712), False, 'from logics.classes.propositional import Inference, Formula\n'), ((796, 810), 'logics.classes.propositional.Formula', 'Formula', (["['B']"], {}), "(['B'])\n", (803, 810), False, 'from logics.classes.propositional import Inference, Formula\n')]