//---------------------------------------------------------------------------

#ifndef ResolutionExperiment1H
#define ResolutionExperiment1H

#include <stdio.h>

class MyClause
{
public:
  __fastcall MyClause();
  __fastcall MyClause(TList *NegativeAtoms, TList *PositiveAtoms);
  __fastcall MyClause(int A1, int A2, int A3, int A4);
  __fastcall ~MyClause();
  bool __fastcall EqualTo(MyClause *Clause2);
  void __fastcall Print(char Title[]);
  TList *NegativeAtoms;
  TList *PositiveAtoms;
};

//---------------------------------------------------------------------------
class MyClauseList
{
public:
  __fastcall MyClauseList();
  __fastcall ~MyClauseList();
  int __fastcall Add(MyClause *newClause); // returns 0 - duplicate found, 1 - OK, 2 - contradiction
  void __fastcall Print(char Title[]);
  TList *Clauses;
  TList *NegativeSingleAtoms;
  TList *PositiveSingleAtoms;
};

//---------------------------------------------------------------------------
void __fastcall MyResolutionExperiment1();

//---------------------------------------------------------------------------
#endif