diff --git a/P3/Task/Propositions.py b/P3/Task/Propositions.py
new file mode 100644
index 0000000..7368349
--- /dev/null
+++ b/P3/Task/Propositions.py
@@ -0,0 +1,284 @@
+from collections import deque
+import re
+
+class HornKnowledgebasedAgent:
+    """Knowledge-based agent using Horn Clauses + Forward Chaining"""
+
+    def __init__(self):
+        """Initialize the agent"""
+        self.knowledge_base = []
+
+    # ==================== MAIN INTERFACE ====================
+
+    def TELL(self, input_data):
+        """Add sensor data from gym step result or legacy string
+
+        Args:
+        input_data: Either string ("S11") or gym step result tuple
+        """
+        # Handle legacy string input
+        if isinstance(input_data, str):
+            self._add_to_kb(input_data)
+            self._auto_generate_rules(input_data)
+            return
+
+        # Handle gym environment step result
+        if isinstance(input_data, tuple) and len(input_data) >= 3:
+            observation, reward, terminated = input_data[0], input_data[1], input_data[2]
+
+            # Extract position (convert 0-based to 1-based)
+            x = observation['x'] + 1
+            y = observation['y'] + 1
+            position = f"{x}{y}"
+
+            print(f"\n🎮 Processing step for position [{x},{y}] - Terminated: {terminated}")
+
+            # Handle death vs survival
+            if terminated:
+                # Agent died - add both Wumpus AND Pit facts (Horn approximation)
+                self._add_to_kb(f"W{position}")
+                self._add_to_kb(f"P{position}")
+                print(f"💀 Death: W{position} ∧ P{position} (Horn approx. of W{position} ∨ P{position})")
+                return
+            else:
+                # Agent survived - field is safe
+                self._add_to_kb(f"-W{position}")
+                self._add_to_kb(f"-P{position}")
+                print(f"✅ Survival: ¬W{position} ∧ ¬P{position}")
+
+            # Process sensors
+            sensors = {
+                'stench': 'S', 'breeze': 'B', 'glitter': 'G',
+                'bump': 'BUMP', 'scream': 'SC'
+            }
+
+            for sensor_key, sensor_code in sensors.items():
+                sensor_value = observation.get(sensor_key, False)
+                if sensor_value:
+                    sensor_fact = f"{sensor_code}{position}"
+                else:
+                    sensor_fact = f"-{sensor_code}{position}"
+
+                print(f"   Sensor: {sensor_fact}")
+                self._add_to_kb(sensor_fact)
+                self._auto_generate_rules(sensor_fact)
+
+    def ASK(self, query):
+        """Check if KB entails query using Forward Chaining"""
+        result = self._forward_chaining(query)
+        print(f"ASK({query}): {result}")
+        return result
+
+    def _add_to_kb(self, sentence):
+        """Add sentence to KB if not already present"""
+        if sentence not in self.knowledge_base:
+            self.knowledge_base.append(sentence)
+            print(f"  Added: {sentence}")
+
+    # ==================== FORWARD CHAINING ====================
+
+    def _forward_chaining(self, query):
+        """Forward Chaining algorithm"""
+        facts, rules = self._parse_kb()
+
+        # Count premises for each rule
+        count = {i: len(rule['premises']) for i, rule in enumerate(rules)}
+
+        # Track inferred symbols
+        inferred = {}
+        derived_facts = set(facts)
+        agenda = deque(facts)
+
+        while agenda:
+            fact = agenda.popleft()
+
+            # Check for contradiction
+            negated = self._negate(fact)
+            if negated in derived_facts:
+                print(f"⚠️  Contradiction: {fact} and {negated}")
+                return False
+
+            # Found query?
+            if fact == query:
+                return True
+
+            # Process rules
+            if not inferred.get(fact, False):
+                inferred[fact] = True
+
+                for i, rule in enumerate(rules):
+                    if fact in rule['premises']:
+                        count[i] -= 1
+                        if count[i] == 0:
+                            conclusion = rule['conclusion']
+                            if not inferred.get(conclusion, False):
+                                agenda.append(conclusion)
+                                derived_facts.add(conclusion)
+
+        # Check if negation of query was derived
+        negated_query = self._negate(query)
+        if negated_query in derived_facts:
+            print(f"  {query} is FALSE (KB entails {negated_query})")
+            return False
+
+        print(f"  {query} cannot be proven")
+        return False
+
+    def _parse_kb(self):
+        """Parse KB into facts and rules"""
+        facts = []
+        rules = []
+
+        for sentence in self.knowledge_base:
+            if '=>' in sentence:
+                premises_part, conclusion = sentence.split('=>')
+                premises = [p.strip() for p in premises_part.split(',')]
+                rules.append({'premises': premises, 'conclusion': conclusion.strip()})
+            else:
+                facts.append(sentence)
+
+        return facts, rules
+
+    def _negate(self, literal):
+        """Negate a literal"""
+        return literal[1:] if literal.startswith('-') else f"-{literal}"
+
+    # ==================== RULE GENERATION ====================
+
+    def _auto_generate_rules(self, sensor):
+        """Generate Horn rules from sensor facts"""
+        # STENCH rules
+        if re.match(r'^S(\d)(\d)$', sensor):
+            x, y = int(sensor[1]), int(sensor[2])
+            pos = f"{x}{y}"
+
+            # S11 => -W11 (no Wumpus in same field)
+            self._add_to_kb(f"S{pos}=>-W{pos}")
+
+            # S11 => W21, S11 => W12 (direct rules for neighbors)
+            for nx, ny in self._get_neighbors(x, y):
+                self._add_to_kb(f"S{pos}=>W{nx}{ny}")
+
+            print(f"    Generated stench rules for S{pos}")
+
+        # NO STENCH rules
+        elif re.match(r'^-S(\d)(\d)$', sensor):
+            x, y = int(sensor[2]), int(sensor[3])
+            pos = f"{x}{y}"
+
+            # -S12 => -W11, -S12 => -W22 (no Wumpus in neighbors)
+            for nx, ny in self._get_neighbors(x, y):
+                self._add_to_kb(f"-S{pos}=>-W{nx}{ny}")
+
+            print(f"    Generated no-stench rules for -S{pos}")
+
+        # BREEZE rules
+        elif re.match(r'^B(\d)(\d)$', sensor):
+            x, y = int(sensor[1]), int(sensor[2])
+            pos = f"{x}{y}"
+
+            # B11 => -P11 (no Pit in same field)
+            self._add_to_kb(f"B{pos}=>-P{pos}")
+
+            # B11 => P21, B11 => P12 (direct rules for neighbors)
+            for nx, ny in self._get_neighbors(x, y):
+                self._add_to_kb(f"B{pos}=>P{nx}{ny}")
+
+            print(f"    Generated breeze rules for B{pos}")
+
+        # NO BREEZE rules
+        elif re.match(r'^-B(\d)(\d)$', sensor):
+            x, y = int(sensor[2]), int(sensor[3])
+            pos = f"{x}{y}"
+
+            # -B12 => -P11, -B12 => -P22 (no Pits in neighbors)
+            for nx, ny in self._get_neighbors(x, y):
+                self._add_to_kb(f"-B{pos}=>-P{nx}{ny}")
+
+            print(f"    Generated no-breeze rules for -B{pos}")
+
+        # GLITTER rules
+        elif re.match(r'^G(\d)(\d)$', sensor):
+            x, y = int(sensor[1]), int(sensor[2])
+            self._add_to_kb(f"G{x}{y}=>Gold{x}{y}")
+            print(f"    Generated glitter rule")
+
+        elif re.match(r'^-G(\d)(\d)$', sensor):
+            x, y = int(sensor[2]), int(sensor[3])
+            self._add_to_kb(f"-G{x}{y}=>-Gold{x}{y}")
+            print(f"    Generated no-glitter rule")
+
+        # SCREAM rules
+        elif sensor == "SC":
+            self._add_to_kb("SC=>WumpusDead")
+            print(f"    Generated scream rule")
+
+        elif sensor == "-SC":
+            self._add_to_kb("-SC=>WumpusAlive")
+            print(f"    Generated no-scream rule")
+
+    def _get_neighbors(self, x, y):
+        """Get valid neighbors in 4x4 grid"""
+        neighbors = []
+        for dx, dy in [(-1,0), (1,0), (0,-1), (0,1)]:
+            nx, ny = x + dx, y + dy
+            if 1 <= nx <= 4 and 1 <= ny <= 4:
+                neighbors.append((nx, ny))
+        return neighbors
+
+    def print_kb(self):
+        """Print knowledge base"""
+        print("\n=== Horn Clauses Knowledge Base ===")
+        facts = [s for s in self.knowledge_base if '=>' not in s]
+        rules = [s for s in self.knowledge_base if '=>' in s]
+
+        print(f"Facts ({len(facts)}):")
+        for i, fact in enumerate(facts, 1):
+            print(f"  {i}. {fact}")
+
+        print(f"Rules ({len(rules)}):")
+        for i, rule in enumerate(rules, 1):
+            print(f"  {i}. {rule}")
+
+
+# ==================== TESTS ====================
+
+def test_horn_gym_integration():
+    """Test Horn agent with gym integration"""
+    print("🎯 Horn Clauses Agent - Gym Integration Test")
+    print("="*50)
+
+    agent = HornKnowledgebasedAgent()
+
+    # Agent survives at [1,1] with stench
+    step_result_1 = (
+        {'x': 0, 'y': 0, 'stench': True, 'breeze': False, 'glitter': False, 'bump': False, 'scream': False},
+        [-1], False, False, {}
+    )
+    agent.TELL(step_result_1)
+
+    # Agent dies at [2,1]
+    step_result_2 = (
+        {'x': 1, 'y': 0, 'stench': False, 'breeze': False, 'glitter': False, 'bump': False, 'scream': False},
+        [-1000], True, False, {}
+    )
+    agent.TELL(step_result_2)
+
+    print("\n🔍 Testing queries:")
+    agent.ASK("W11")    # Should be FALSE (survived)
+    agent.ASK("P11")    # Should be FALSE (survived)
+    agent.ASK("W21")    # Should be TRUE (died)
+    agent.ASK("P21")    # Should be False No breez at 11
+    agent.ASK("W12")    # Should be TRUE (from S11)
+    agent.ASK("W22")    # Should be TRUE (from S11)
+
+    agent.print_kb()
+
+if __name__ == "__main__":
+    print("🏰 Horn Clauses Agent for Wumpus World")
+    print("="*60)
+
+    test_horn_gym_integration()
+
+    print("\n✨ Horn implementation complete!")
+    print("   Shows clear limitations vs CNF Resolution")
\ No newline at end of file
diff --git a/P3/Task/Propositions2.py b/P3/Task/Propositions2.py
new file mode 100644
index 0000000..05f3872
--- /dev/null
+++ b/P3/Task/Propositions2.py
@@ -0,0 +1,411 @@
+from collections import deque
+import re
+
+
+class KnowledgebasedAgent:
+    """Knowledge-based agent for Wumpus World using CNF Resolution"""
+
+    def __init__(self, method="CNF"):
+        """Initialize the knowledge-based agent"""
+        self.method = method
+        self.cnf_clauses = []  # List of sets (each set is a clause)
+
+    # ==================== MAIN INTERFACE ====================
+
+    def TELL(self, step_result):
+        """Add sensor data from gym environment step result
+        Args:
+        step_result: Can be either:
+        - String (legacy): "S11", "-B12", etc.
+        - Tuple from env.step(): (observation, reward, terminated, truncated, info)
+        """
+        # Handle legacy string input
+        if isinstance(step_result, str):
+            # print(f"Added sensor: {step_result}")
+            self._generate_clauses_from_sensor(step_result)
+            return
+
+        # Handle gym environment step result
+        if isinstance(step_result, tuple) and len(step_result) >= 3:
+            observation, reward, terminated = step_result[0], step_result[1], step_result[2]
+
+            # Extract position (convert from 0-based to 1-based coordinates)
+            x = observation['x'] + 1  # Convert 0-based to 1-based
+            y = observation['y'] + 1  # Convert 0-based to 1-based
+            position = f"{x}{y}"
+
+            print(f"\n  Processing step result for position [{x},{y}]:")
+            print(f"  Terminated: {terminated}, Reward: {reward}")
+
+            # Extract sensors from observation
+            sensors = {
+                'stench': observation.get('stench', False),
+                'breeze': observation.get('breeze', False),
+                'glitter': observation.get('glitter', False),
+                'bump': observation.get('bump', False),
+                'scream': observation.get('scream', False)
+            }
+
+            # Process survival/death logic first
+            if terminated:
+                # Agent died - field contains Wumpus OR Pit
+                death_clause = {f"W{position}", f"P{position}"}
+                self.cnf_clauses.append(death_clause)
+                print(f"   Death rule: W{position} ∨ P{position}")
+
+                # No sensor processing when agent dies
+                print(f"   Agent died - no sensor data processed")
+                return
+            else:
+                # Agent survived - field is safe (no Wumpus AND no Pit)
+                safe_wumpus = {f"-W{position}"}
+                safe_pit = {f"-P{position}"}
+                self.cnf_clauses.append(safe_wumpus)
+                self.cnf_clauses.append(safe_pit)
+                print(f"  Survival rules: ¬W{position} ∧ ¬P{position}")
+
+            # Process sensor readings
+            sensor_mapping = {
+                'stench': 'S',
+                'breeze': 'B',
+                'glitter': 'G',
+                'bump': 'BUMP',
+                'scream': 'SC'
+            }
+
+            for sensor_name, sensor_value in sensors.items():
+                sensor_code = sensor_mapping.get(sensor_name, sensor_name.upper())
+
+                if sensor_value:
+                    # Positive sensor reading
+                    sensor_fact = f"{sensor_code}{position}"
+                    # print(f"   Sensor: {sensor_fact}")
+                    self._add_sensor_unit_clause(sensor_fact)
+                    self._generate_clauses_from_sensor(sensor_fact)
+                else:
+                    # Negative sensor reading
+                    sensor_fact = f"-{sensor_code}{position}"
+                    # print(f"   Sensor: {sensor_fact}")
+                    self._add_sensor_unit_clause(sensor_fact)
+                    self._generate_clauses_from_sensor(sensor_fact)
+
+            return
+
+    def _add_sensor_unit_clause(self, sensor_fact):
+        """Add sensor as unit clause (avoid duplicates from _generate_clauses_from_sensor)"""
+        unit_clause = {sensor_fact}
+        if unit_clause not in self.cnf_clauses:
+            self.cnf_clauses.append(unit_clause)
+
+    def TELL_SENSOR(self, sensor_string):
+        """Legacy method for adding individual sensor strings"""
+        self.TELL(sensor_string)
+
+    def TELL_STEP(self, step_result):
+        """Convenience method specifically for gym step results"""
+        self.TELL(step_result)
+
+    def ASK(self, query):
+        """Check if KB entails query using CNF Resolution"""
+        result = self._cnf_resolution(query)
+        print(f"ASK({query}): {result}")
+        return result
+
+    def print_clauses(self):
+        """Print all CNF clauses"""
+        print("\n=== CNF Clauses ===")
+        for i, clause in enumerate(self.cnf_clauses):
+            literals = " ∨ ".join(sorted(clause))
+            print(f"  {i + 1}. {{{literals}}}")
+
+    # ==================== CNF RESOLUTION ALGORITHM ====================
+
+    def _cnf_resolution(self, query):
+        """CNF Resolution to prove KB |= query"""
+        # To prove KB |= query, show KB ∧ ¬query is unsatisfiable
+        negated_query = self._negate(query)
+        test_clauses = [clause.copy() for clause in self.cnf_clauses]
+        test_clauses.append({negated_query})
+
+        print(f"\nProving: KB ∧ ¬{query} is unsatisfiable")
+        print(f"Added negated query: {{{negated_query}}}")
+
+        new_clauses = []
+        iteration = 0
+
+        while True:
+            iteration += 1
+            # print(f"\n--- Resolution Step {iteration} ---")
+
+            # Try all pairs of clauses
+            for i in range(len(test_clauses)):
+                for j in range(i + 1, len(test_clauses)):
+                    resolvent = self._resolve(test_clauses[i], test_clauses[j])
+
+                    if resolvent is not None:
+                        if len(resolvent) == 0:
+                            # Empty clause = contradiction!
+                            print(f"Empty clause from {test_clauses[i]} ∩ {test_clauses[j]}")
+                            print("⚡ Contradiction found! KB entails query.")
+                            return True
+
+                        # Check if new clause is actually new
+                        if resolvent not in test_clauses and resolvent not in new_clauses:
+                            new_clauses.append(resolvent)
+                            # print(f"New: {resolvent} from {test_clauses[i]} ∩ {test_clauses[j]}")
+
+            # If no new clauses, we're done
+            if not new_clauses:
+                print("No new clauses. Query not entailed.")
+                return False
+
+            # Add new clauses
+            test_clauses.extend(new_clauses)
+            new_clauses = []
+
+            # Safety limit
+            if iteration > 20:
+                print("Max iterations reached.")
+                return False
+
+    def _resolve(self, clause1, clause2):
+        """Resolve two clauses if they have complementary literals"""
+        for literal in clause1:
+            complement = self._negate(literal)
+            if complement in clause2:
+                # Found resolution: combine clauses, remove complementary pair
+                resolvent = (clause1 - {literal}) | (clause2 - {complement})
+                return resolvent
+        return None
+
+    # ==================== SENSOR RULE GENERATION ====================
+
+    def _generate_clauses_from_sensor(self, sensor):
+        """Generate CNF clauses based on sensor readings"""
+        # Add sensor as unit clause
+        self.cnf_clauses.append({sensor})
+
+        # Dispatch to specific sensor handlers
+        if self._handle_stench_sensors(sensor): return
+        if self._handle_breeze_sensors(sensor): return
+        if self._handle_glitter_sensors(sensor): return
+        if self._handle_scream_sensors(sensor): return
+        if self._handle_bump_sensors(sensor): return
+
+    def _handle_stench_sensors(self, sensor):
+        """Handle stench-related sensors"""
+        # STENCH: S11, S22, etc.
+        stench_match = re.match(r'^S(\d)(\d)$', sensor)
+        if stench_match:
+            x, y = int(stench_match.group(1)), int(stench_match.group(2))
+            pos = f"{x}{y}"
+
+            # S11 → ¬W11 becomes {-S11, -W11}
+            self.cnf_clauses.append({f"-S{pos}", f"-W{pos}"})
+
+            # S11 → (W21 ∨ W12 ∨ ...) becomes {-S11, W21, W12, ...}
+            neighbors = self._get_neighbors(x, y)
+            if neighbors:
+                neighbor_wumpus = [f"W{nx}{ny}" for nx, ny in neighbors]
+                clause = {f"-S{pos}"} | set(neighbor_wumpus)
+                self.cnf_clauses.append(clause)
+
+            print(f"  Generated: S{pos} → ¬W{pos} ∧ (W-neighbors)")
+            return True
+
+        # NO STENCH: -S12, -S22, etc.
+        no_stench_match = re.match(r'^-S(\d)(\d)$', sensor)
+        if no_stench_match:
+            x, y = int(no_stench_match.group(1)), int(no_stench_match.group(2))
+            pos = f"{x}{y}"
+
+            # -S12 → ¬W(neighbors) becomes {S12, -W11}, {S12, -W22}, etc.
+            neighbors = self._get_neighbors(x, y)
+            for nx, ny in neighbors:
+                neighbor_pos = f"{nx}{ny}"
+                self.cnf_clauses.append({f"S{pos}", f"-W{neighbor_pos}"})
+
+            print(f"  Generated: ¬S{pos} → ¬W-neighbors")
+            return True
+
+        return False
+
+    def _handle_breeze_sensors(self, sensor):
+        """Handle breeze-related sensors"""
+        # BREEZE: B11, B22, etc.
+        breeze_match = re.match(r'^B(\d)(\d)$', sensor)
+        if breeze_match:
+            x, y = int(breeze_match.group(1)), int(breeze_match.group(2))
+            pos = f"{x}{y}"
+
+            # B11 → ¬P11 becomes {-B11, -P11}
+            self.cnf_clauses.append({f"-B{pos}", f"-P{pos}"})
+
+            # B11 → (P21 ∨ P12 ∨ ...) becomes {-B11, P21, P12, ...}
+            neighbors = self._get_neighbors(x, y)
+            if neighbors:
+                neighbor_pits = [f"P{nx}{ny}" for nx, ny in neighbors]
+                clause = {f"-B{pos}"} | set(neighbor_pits)
+                self.cnf_clauses.append(clause)
+
+            print(f"  Generated: B{pos} → ¬P{pos} ∧ (P-neighbors)")
+            return True
+
+        # NO BREEZE: -B12, -B22, etc.
+        no_breeze_match = re.match(r'^-B(\d)(\d)$', sensor)
+        if no_breeze_match:
+            x, y = int(no_breeze_match.group(1)), int(no_breeze_match.group(2))
+            pos = f"{x}{y}"
+
+            # -B12 → ¬P(neighbors) becomes {B12, -P11}, {B12, -P22}, etc.
+            neighbors = self._get_neighbors(x, y)
+            for nx, ny in neighbors:
+                neighbor_pos = f"{nx}{ny}"
+                self.cnf_clauses.append({f"B{pos}", f"-P{neighbor_pos}"})
+
+            print(f"  Generated: ¬B{pos} → ¬P-neighbors")
+            return True
+
+        return False
+
+    def _handle_glitter_sensors(self, sensor):
+        """Handle glitter-related sensors"""
+        # GLITTER: G11, G22, etc.
+        glitter_match = re.match(r'^G(\d)(\d)$', sensor)
+        if glitter_match:
+            x, y = int(glitter_match.group(1)), int(glitter_match.group(2))
+            pos = f"{x}{y}"
+
+            # G11 → Gold11 becomes {-G11, Gold11}
+            self.cnf_clauses.append({f"-G{pos}", f"Gold{pos}"})
+            print(f"  Generated: G{pos} → Gold{pos}")
+            return True
+
+        # NO GLITTER: -G11, -G22, etc.
+        no_glitter_match = re.match(r'^-G(\d)(\d)$', sensor)
+        if no_glitter_match:
+            x, y = int(no_glitter_match.group(1)), int(no_glitter_match.group(2))
+            pos = f"{x}{y}"
+
+            # -G11 → ¬Gold11 becomes {G11, -Gold11}
+            self.cnf_clauses.append({f"G{pos}", f"-Gold{pos}"})
+            print(f"  Generated: ¬G{pos} → ¬Gold{pos}")
+            return True
+
+        return False
+
+    def _handle_scream_sensors(self, sensor):
+        """Handle scream-related sensors"""
+        # SCREAM: Sc
+        if sensor == "Sc":
+            # Sc → WumpusDead becomes {-Sc, WumpusDead}
+            self.cnf_clauses.append({"-Sc", "WumpusDead"})
+            # WumpusDead → ¬W_anywhere: for all positions
+            for x in range(1, 5):
+                for y in range(1, 5):
+                    self.cnf_clauses.append({"-WumpusDead", f"-W{x}{y}"})
+            print(f"  Generated: Sc → WumpusDead → ¬W(everywhere)")
+            return True
+
+        # NO SCREAM: -Sc
+        if sensor == "-Sc":
+            # -Sc → WumpusAlive becomes {Sc, WumpusAlive}
+            self.cnf_clauses.append({"Sc", "WumpusAlive"})
+            print(f"  Generated: ¬Sc → WumpusAlive")
+            return True
+
+        return False
+
+    def _handle_bump_sensors(self, sensor):
+        """Handle bump-related sensors"""
+        # BUMP: Bump11, Bump22, etc.
+        bump_match = re.match(r'^Bump(\d)(\d)$', sensor)
+        if bump_match:
+            x, y = int(bump_match.group(1)), int(bump_match.group(2))
+            print(f"  Note: Bump{x}{y} indicates wall collision")
+            return True
+
+        # NO BUMP: -Bump11, -Bump22, etc.
+        no_bump_match = re.match(r'^-Bump(\d)(\d)$', sensor)
+        if no_bump_match:
+            x, y = int(no_bump_match.group(1)), int(no_bump_match.group(2))
+            print(f"  Note: ¬Bump{x}{y} indicates successful movement")
+            return True
+
+        return False
+
+    # ==================== UTILITY METHODS ====================
+
+    def _negate(self, literal):
+        """Negate a literal"""
+        if literal.startswith('-'):
+            return literal[1:]
+        else:
+            return f"-{literal}"
+
+    def _get_neighbors(self, x, y):
+        """Get valid neighbors in 4x4 grid"""
+        neighbors = []
+        for dx, dy in [(-1, 0), (1, 0), (0, -1), (0, 1)]:
+            nx, ny = x + dx, y + dy
+            if 1 <= nx <= 4 and 1 <= ny <= 4:
+                neighbors.append((nx, ny))
+        return neighbors
+
+
+# ==================== TEST SCENARIOS ====================
+
+
+def test_gym_integration():
+    """Test direct integration with gym environment step results"""
+    print("\n🎮 Test 3: Direct Gym Environment Integration")
+    print("="*60)
+
+    agent = KnowledgebasedAgent("CNF")
+
+    print("📡 Simulating gym environment step results...")
+
+    # Simulate step result from your example
+    step_result_1 = (
+        {'x': 0, 'y': 0, 'gold': False, 'direction': 1, 'arrow': True,
+         'stench': True, 'breeze': False, 'glitter': False, 'bump': False, 'scream': False},
+        [-1],     # reward
+        False,    # terminated (agent survives)
+        False,    # truncated
+        {'info': 'step 1'}
+    )
+
+    # Agent survives at position [1,1] (converted from [0,0])
+    agent.TELL(step_result_1)
+
+    # Simulate death scenario
+    step_result_2 = (
+        {'x': 1, 'y': 0, 'gold': False, 'direction': 1, 'arrow': True,
+         'stench': False, 'breeze': False, 'glitter': False, 'bump': False, 'scream': False},
+        [-1000],  # death reward
+        True,     # terminated (agent dies)
+        False,    # truncated
+        {'info': 'death'}
+    )
+
+    # Agent dies at position [2,1] (converted from [1,0])
+    agent.TELL(step_result_2)
+
+    print("\n🔍 Testing queries with survival logic...")
+    agent.ASK("W11")      # Should be FALSE (agent survived [1,1])
+    agent.ASK("P11")      # Should be FALSE (agent survived [1,1])
+    agent.ASK("W21")      # Could be TRUE (agent died at [2,1])
+    agent.ASK("P21")      # Should be False (no breez at [1,1])
+
+    print("\n📋 Generated clauses:")
+    agent.print_clauses()
+
+
+
+if __name__ == "__main__":
+    print("🏰 CNF Resolution for Wumpus World - Complete Implementation")
+    print("=" * 70)
+
+    test_gym_integration()
+
+    print("\n✨ CNF Resolution correctly handles all Wumpus World logic!")
diff --git a/P3/Task/__pycache__/Propositions.cpython-310.pyc b/P3/Task/__pycache__/Propositions.cpython-310.pyc
new file mode 100644
index 0000000..dff50c7
Binary files /dev/null and b/P3/Task/__pycache__/Propositions.cpython-310.pyc differ
diff --git a/P3/Task/__pycache__/Propositions2.cpython-310.pyc b/P3/Task/__pycache__/Propositions2.cpython-310.pyc
new file mode 100644
index 0000000..d0e8c88
Binary files /dev/null and b/P3/Task/__pycache__/Propositions2.cpython-310.pyc differ
diff --git a/P3/Wumpus_Test.py b/P3/Wumpus_Test.py
deleted file mode 100644
index e69de29..0000000
diff --git a/P3/ai_gym b/P3/ai_gym
new file mode 160000
index 0000000..aa0a38e
--- /dev/null
+++ b/P3/ai_gym
@@ -0,0 +1 @@
+Subproject commit aa0a38ebaf6b0ea63cf206dfa0586a82bdb9ec85
diff --git a/P3/main.py b/P3/main.py
new file mode 100644
index 0000000..9cb81fd
--- /dev/null
+++ b/P3/main.py
@@ -0,0 +1,75 @@
+import random
+import gym
+from ai_gym import fh_ac_ai_gym
+from Task.Propositions import *
+from Task.Propositions2 import *
+
+#Create Gym environment
+wumpus_env = gym.make('Wumpus-v0', disable_env_checker=True)
+wumpus_env.reset()
+wumpus_env.render()
+
+#Define the possible actions
+REVERSE_ACTION_DICT= {0: "WALK", 1:"TURNLEFT", 2:"TURNRIGHT", 3:"GRAB", 4: "SHOOT", 5:"CLIMB"}
+POSSIBLE_ACTIONS = {v: k for k, v in REVERSE_ACTION_DICT.items()}
+
+
+print("=" * 70)
+
+agent = KnowledgebasedAgent("CNF")
+obs = wumpus_env.step(1)
+print(obs)
+agent.TELL(obs)
+agent.ASK("W21")
+agent.ASK("W12")
+wumpus_env.render()
+
+print("=" * 70)
+obs = wumpus_env.step(0)
+print(obs)
+agent.TELL(obs)
+agent.ASK("W21")
+agent.ASK("W12")
+wumpus_env.render()
+
+print("=" * 70)
+obs = wumpus_env.step(0)
+print(obs)
+agent.TELL(obs)
+agent.ASK("P12")
+agent.ASK("P23")
+agent.ASK("P14")
+wumpus_env.render()
+
+print("=" * 70)
+wumpus_env.step(2)
+obs = wumpus_env.step(0)
+print(obs)
+agent.TELL(obs)
+agent.ASK("P12")
+agent.ASK("P23")
+agent.ASK("P14")
+wumpus_env.render()
+
+wumpus_env.reset()
+print("=" * 70)
+print("=" * 70)
+print("=" * 70)
+
+
+agent = HornKnowledgebasedAgent()
+wumpus_env.step(1)
+obs = wumpus_env.step(2)
+print(obs)
+agent.TELL(obs)
+agent.ASK("W21")
+agent.ASK("W12")
+wumpus_env.render()
+
+print("=" * 70)
+obs = wumpus_env.step(0)
+print(obs)
+agent.TELL(obs)
+agent.ASK("W21")
+agent.ASK("W12")
+wumpus_env.render()