#include <iostream>
#include <fstream>
#include <vector>
#include <algorithm>
#include <assert.h>

using namespace std;

typedef int Literal;
typedef vector<Literal> Valuation;

class Clause
{
public:
  Clause(vector<Literal>& literals)
    : _literals(literals)
  {
  }
  
  Clause(const Clause& clause)
  {
    _literals=clause._literals;
  }
  
  bool empty()
  {
    return _literals.size()==0;
  }
  
  bool unit()
  {
    return _literals.size()==1;
  }
  
  Literal operator[](int i)
  {
    return _literals[i];
  }
  
  bool isTrue(Valuation& v)
  {
    for(int i=0; i<_literals.size(); i++)
    {
      for(int j=i+1; j<_literals.size(); j++)
        if(_literals[i]==-_literals[j])
          return true;
      if(find(v.begin(),v.end(),_literals[i])!=v.end())
        return true;
    }
    return false;
  }
  
  Clause removeFalseLiterals(Valuation& v)
  {
    vector<Literal> literals;
    for(int i=0; i<_literals.size(); i++)
      if(find(v.begin(),v.end(),-_literals[i])==v.end())
        literals.push_back(_literals[i]);
    return Clause(literals);
  }
  
private:
  vector<Literal> _literals;
};

class Formula
{
public:
  Formula(vector<Clause>& clauses, int maxVariable)
    : _clauses(clauses), _maxVariable(maxVariable)
  {
  }
  
  Formula(char* filename)
  {
    ifstream in(filename);
    string p, cnf;
    int nClauses;
    in >> p >> cnf >> _maxVariable >> nClauses;
    vector<Literal> literals;
    for(int i=0; i<nClauses; i++)
    {
      Literal l;
      literals.clear();
      in >> l;
      while(l!=0)
      {
        literals.push_back(l);
        in >> l;
      }
      _clauses.push_back(Clause(literals));
    }
  }
  
  bool empty()
  {
    return _clauses.size()==0;
  }
  
  bool containsEmptyClause()
  {
    for(int i=0; i<_clauses.size(); i++)
      if(_clauses[i].empty())
        return true;
    return false;
  }
  
  Literal getUnitLiteral()
  {
    for(int i=0; i<_clauses.size(); i++)
      if(_clauses[i].unit())
        return _clauses[i][0];
    return 0;
  }
  
  Literal getUndefinedVariable(Valuation& v)
  {
    for(int i=1; i<=_maxVariable; i++)
      if(find(v.begin(),v.end(),i)==v.end() && 
        find(v.begin(),v.end(),-i)==v.end())
        return i;
    return 0;
  }
  
  Formula simplify(Valuation& v)
  {
    vector<Clause> clauses;
    for(int i=0; i<_clauses.size(); i++)
      if(!_clauses[i].isTrue(v))
        clauses.push_back(_clauses[i].removeFalseLiterals(v));
    return Formula(clauses,_maxVariable);
  }
  
private:
  vector<Clause> _clauses;
  int _maxVariable;
};

class Solver
{
public:
  bool solve(Formula formula)
  {
    if(formula.empty())
    {
      _satisfyingValuation=_currentValuation;
      return true;
    }
    if(formula.containsEmptyClause())
      return false;
    Literal l;
    l=formula.getUnitLiteral();
    if(l!=0)
    {
      _currentValuation.push_back(l);
      bool val=solve(formula.simplify(_currentValuation));
      _currentValuation.pop_back();
      return val;
    }
    l=formula.getUndefinedVariable(_currentValuation);
    assert(l!=0);
    _currentValuation.push_back(l);
    bool val=solve(formula.simplify(_currentValuation));
    _currentValuation.pop_back();
    if(val==true)
      return true;
    else
    {
      _currentValuation.push_back(-l);
      bool val=solve(formula.simplify(_currentValuation));
      _currentValuation.pop_back();
      return val;
    }        
  }
  void printValuation()
  {
    for(int i=0; i<_satisfyingValuation.size(); i++)
      cout << _satisfyingValuation[i] << " ";
    cout << endl;
  }
private:
  Valuation _currentValuation;
  Valuation _satisfyingValuation;
};


int main(int argc, char** argv)
{
  if(argc<2)
  {
    cerr << "Nedostaje argument!" << endl;
    exit(1);
  }
  Formula formula(argv[1]);
  Solver solver;
  if(solver.solve(formula))
    solver.printValuation();
  else
    cout << "Unsatisfiable" << endl;
  return 0;
}