public void unfoldTBox() {
		// TODO Auto-generated method stub
	  HashMap<OWLClassExpression, Concept> axioms=kb.getSubAxiom();	
	  Set<OWLClassExpression> ens=axioms.keySet();
	  Iterator iter=ens.iterator();
	  int size;
      while(iter.hasNext()){
    	  //System.out.println(tableaux.size());
		  OWLClassExpression cl= (OWLClassExpression)iter.next();
		  OWLClassExpression crO= axioms.get(cl).getExpression();
		  String type = crO.getClassExpressionType().toString();
		  OWLClassExpression cr;
		  if(type.equals("ObjectComplementOF")){
			  OWLObjectComplementOf expComp1=(OWLObjectComplementOf)crO;
			  cr=expComp1.getOperand();
		  }
		  else{
			  cr=crO.getComplementNNF();
		  }
		  size=getSize();
    	  for(int j=0;j<size;j++){
    		  if(!tableaux.get(j).hasChild()){
    			  Noeud left=new Noeud(getSize()+1);
    			  Noeud right=new Noeud(getSize()+2);
    			  left.initCopyT(tableaux.get(j).getLabelT());
    			  left.initCopyF(tableaux.get(j).getLabelF());
    			  right.initCopyT(tableaux.get(j).getLabelT());
    			  right.initCopyF(tableaux.get(j).getLabelF());
    			  left.addLabelF(cl);
    			  right.addLabelF(cr);
    			  tableaux.get(j).addChild(left);
    			  tableaux.get(j).addChild(right);
    			  left.addParent(tableaux.get(j));
    			  right.addParent(tableaux.get(j));
    			  tableaux.add(left);
    			  tableaux.add(right);
    		  }
    	  }
    	  
      }
	}