public int callProbLogicEval(boolean addRules, boolean poTypedWD, Report report, int numberPo,
			String parameters, String goalExpression) {

		exitVal = 0;

		try {
			Runtime rt = Runtime.getRuntime();

			String tmpPath = System.getProperty("java.io.tmpdir");
			String tmpFileName = tmpPath + File.separator + moduleName + "_"
					+ expressionName + ".goal";

			writeFile(tmpFileName, goalExpression);

			long initial_time = System.currentTimeMillis();
			
			//JOptionPane.showMessageDialog(null,goalExpression);
					
			//JOptionPane.showMessageDialog(null, this.getExecutablePath() + " "+ parameters.replace("\n", " ") + " --eval_rule_file "+ tmpFileName);
			
			Process proc = rt.exec(this.getExecutablePath() + " "
					+ parameters.replace("\n", " ") + " --eval_rule_file "
					+ tmpFileName);

			// any error message?
			StreamGobbler errorGobbler = new StreamGobbler(
					proc.getErrorStream(), "ERROR");

			// any output?
			StreamGobbler outputGobbler = new StreamGobbler(
					proc.getInputStream(), "OUTPUT"); // Can add a new parameter , System.out

			// kick them off
			errorGobbler.start();
			outputGobbler.start();

			exitVal = proc.waitFor();
			// Final time
			total_time = System.currentTimeMillis() - initial_time;

			Result res_out, res_error;
			res_out = outputGobbler.getResult();
			res_error = errorGobbler.getResult();

			//It is used to identify when the evaluation is individual
			String stateProB="";
			if(numberPo!=0)
				stateProB = posManager.getProofState(numberPo);
				
			report.add(numberPo,
					parameters,
					POWD.Common,
					PoGenerated.Full,
					goalExpression,
					stateProB,
					res_error,
					res_out,
					total_time);
			
			
			if (res_out != Result.ERROR && res_error != Result.ERROR) {
				printSuccessFullyMsg();
				result = res_out;

				if (result == Result.TRUE && addRules) {
					
					if(numberPo==0){ // It is used only in interactive prover - 
						posManager.addOneRuleInPMMFile(poTypedWD,goal+"==btrue",expressionName,total_time);
					}else{
						// This rule is used to add true rules of component
						
						String name = stateAndNames[numberPo-1];//.replaceAll(" ", "").replaceAll("\n", "").substring(stateAndNames[numberPo-1].indexOf("-")).substring(0, stateAndNames[numberPo-1].indexOf("(") );
						
						String userPass= "Operation("+name.substring(0,name.lastIndexOf("_"))+") & mp(Tac(RulesProB"	+name+"))";
								
					    String addedRule = new String(  "THEORY RulesProB"
								+ name+ " IS \n\n"
								+ "\n\t /* Expression from (" + name
								+ "), it was added  in " + new Date()
								+ "\n\t  evaluated with ProB in " + total_time + " milliseconds"
								+ "\n\t  Module Path:" + modulePath + " */" + "\n\n\t " + posManager.getProofObligationsWithLocalHypotheses(numberPo) 
								+ "\nEND\n");
						
						posManager.addTheoryAndUserPassInList(addedRule , userPass);

					}
				}

			} else {
				result = res_error;
				exitVal = 1;
			}

			System.out.println("Time spent: " + total_time);
			System.out.println("Process exit value: " + exitVal);

		} catch (Throwable t) {
			t.printStackTrace();
		}
		return exitVal;

	}