public static boolean solve(KBase kb, Clause goal, Substitution[] sub)
{//???????   All yours 	??????????
/*	kb is a knowledge base of Horn clauses. The parameter goal is 
a non-empty clause without positive literal. On return, sub[0] will 
contain the combined substitution from the goal to an empty clause {}.
The sub[0] is related to the "answer extraction" page 261, when 
the goal can be solved. Return true if the empty clause is found, 
so sub[0] can be used to extract answers to the goal.	
Furthermore, this method uses depth first search, use set of support 
and Liner input strategy. It always works at the first literal 
in the subgoal. It follows the order of clauses in kb when doing 
depth first-search. Solve returns false if there is no place to backtrack to.*/
	Clause[] resolv=new Clause[1];
	resolv[0]=new Clause();
	Clause subgoal = goal;
  int start=0;
	Stack goals = new Stack();
	Stack subs = new Stack();
	Stack positions = new Stack();
	boolean done=false;
	
	while (!done) {
			// for each clauses in knowledge base
			for(int c=start; c < kb.size(); c++) { 
			   int position=-1;
			
				// find pos literal with the same predicate symbol of
				// literal in the goal
				for(int l=0; l < kb.elementAt(c).size(); l++) { 
					if(subgoal.elementAt(0).getPredSym().isSame(
							kb.elementAt(c).elementAt(l).getPredSym()) && 
							(!kb.elementAt(c).elementAt(l).negative()))
							{	position=l;	}
				}
				
				// if a resolvent
				if (position > -1 && 
					resolutionHorn(subgoal,kb.elementAt(c),sub,resolv,position))
				{
					if (resolv[0].size() == 0) {
						System.out.println("Empty Resolvent!!");
						while (subs.size() != 0) {
							Substitution curr=(Substitution)subs.pop();
							System.out.println(curr.toString());
						}
						done=true;
					}	else {
						subs.push(sub[0]);
						
						String newgoal=resolv[0].toString().
						substring(0,resolv[0].toString().indexOf("\n"));
						System.out.println(
						  "Resolvent found at clause "+c+" new subgoal is "+newgoal+"!!"
						);						
						positions.push(new Integer(c));
						goals.push(subgoal);
						subgoal=resolv[0];
						//start=0;
					}
				} else if (position > -1) {
					subs.pop();
					Integer S =(Integer)positions.pop();
					start = S.intValue();
					subgoal=(Clause)goals.pop();
					System.out.println("End of Branch Popping...");
			}
		}
	} // end while
	return true;
}