from backend.core.universe_generator import UniverseGenerator
from backend.core.theorem_engine import TheoremEngine
from backend.db.session import SessionLocal

def test_theorem_derivation():
    db = SessionLocal()
    generator = UniverseGenerator(db)
    universe = generator.create_universe("Thm Universe", "For theorem derivation", "generic", ["Closure", "Associativity"])
    axiom1 = generator.add_axiom(universe.id, "Closure")
    axiom2 = generator.add_axiom(universe.id, "Associativity")
    engine = TheoremEngine(db)
    theorem = engine.derive_theorem(universe.id, [axiom1.id, axiom2.id], "Closure Associativity")
    assert theorem.statement == "Closure Associativity"
    assert "Derived from axioms" in theorem.proof
    db.close()