Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

export BK_INPUT=DotAndBoxes-COL-2
export BK_EXAMINATION=ReachabilityFireability
export BK_TOOL=ITS-Tools
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1753
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/DotAndBoxes-COL-2
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool ITS-Tools:'
echo ' Test is DotAndBoxes-COL-2, examination is ReachabilityFireability'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of ITS-Tools for DotAndBoxes/2 (Colored)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

execution on node 40: cluster1u42.lip6.fr (runId=136937310001241_n_40)
=====================================================================
runnning ITS-Tools on DotAndBoxes-COL-2 (ReachabilityFireability)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool ITS-Tools:
Test is DotAndBoxes-COL-2, examination is ReachabilityFireability
=====================================================================

--------------------
content from stdout:

START 1370115868
/home/mcc/BenchKit/bin/its-reach -i model.sep.flat.gal -t GAL --quiet -reachable-file ReachabilityFireability.flat.prop --nowitness
FORMULA p_2_fireability_and FALSE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_3_fireability_or FALSE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_4_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_5_fireability_or_notx FALSE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_6_fireability_x TRUE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_48_fireability_and TRUE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_49_fireability_or TRUE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
FORMULA p_50_fireability_and_notx FALSE TECHNIQUES DECISION_DIAGRAMS STRUCTURAL_REDUCTIONS
STOP 1370115868

--------------------
content from stderr:

initial cost 1990
final cost 927
Eval1[11],End[0],Eval1[5],Chosed[1],Eval1[2],FreePositions[1],OccupiedPositions[1],Eval1[0],Chosed[9],FreePositions[0],Chosed[0],FreePositions[4],Eval1[13],End[1],Eval1[10],FreePositions[2],Eval1[12],Chosed[12],Eval1[4],FreePositions[5],Chosed[4],Chosed[3],IsWinner[0],OccupiedPositions[3],Chosed[2],FreePositions[3],IsWinner[1],Idle[0],Chosed[11],Chosed[10],OccupiedPositions[2],OccupiedPositions[4],OccupiedPositions[0],Chosed[5],Eval1[1],OccupiedPositions[5],Idle[1],Eval1[6],IsWinner[3],IsWinner[2],Chosed[8],Eval1[8],Chosed[13],Eval1[9],Eval1[14],Chosed[6],FreePositions[6],OccupiedPositions[6],Chosed[14],Chosed[7],FreePositions[7],OccupiedPositions[7],Chosed[15],Score[1],Score[0],Score[2],Score[4],Score[3],Eval1[3],Eval1[15],Score[6],Score[5],Eval1[7],Score[7],Score[9],Score[8],
Read property : p_2_fireability_and with value :false
Read property : p_3_fireability_or with value :Idle[0] >= 1 && FreePositions[0] >= 1 || Idle[1] >= 1 && FreePositions[0] >= 1 || Idle[0] >= 1 && FreePositions[4] >= 1 || Idle[1] >= 1 && FreePositions[4] >= 1 || Idle[0] >= 1 && FreePositions[2] >= 1 || Idle[1] >= 1 && FreePositions[2] >= 1 || Idle[0] >= 1 && FreePositions[6] >= 1 || Idle[1] >= 1 && FreePositions[6] >= 1 || Idle[0] >= 1 && FreePositions[1] >= 1 || Idle[1] >= 1 && FreePositions[1] >= 1 || Idle[0] >= 1 && FreePositions[5] >= 1 || Idle[1] >= 1 && FreePositions[5] >= 1 || Idle[0] >= 1 && FreePositions[3] >= 1 || Idle[1] >= 1 && FreePositions[3] >= 1 || Idle[0] >= 1 && FreePositions[7] >= 1 || Idle[1] >= 1 && FreePositions[7] >= 1 || (End[0] >= 1 && IsWinner[1] >= 1 || End[1] >= 1 && IsWinner[3] >= 1)
Read property : p_4_fireability_and_notx with value :false
Read property : p_5_fireability_or_notx with value :Idle[0] >= 1 && FreePositions[0] >= 1 || Idle[1] >= 1 && FreePositions[0] >= 1 || Idle[0] >= 1 && FreePositions[4] >= 1 || Idle[1] >= 1 && FreePositions[4] >= 1 || Idle[0] >= 1 && FreePositions[2] >= 1 || Idle[1] >= 1 && FreePositions[2] >= 1 || Idle[0] >= 1 && FreePositions[6] >= 1 || Idle[1] >= 1 && FreePositions[6] >= 1 || Idle[0] >= 1 && FreePositions[1] >= 1 || Idle[1] >= 1 && FreePositions[1] >= 1 || Idle[0] >= 1 && FreePositions[5] >= 1 || Idle[1] >= 1 && FreePositions[5] >= 1 || Idle[0] >= 1 && FreePositions[3] >= 1 || Idle[1] >= 1 && FreePositions[3] >= 1 || Idle[0] >= 1 && FreePositions[7] >= 1 || Idle[1] >= 1 && FreePositions[7] >= 1 || (End[0] >= 1 && IsWinner[1] >= 1 || End[1] >= 1 && IsWinner[3] >= 1)
Read property : p_6_fireability_x with value :! (End[0] >= 1 && IsWinner[1] >= 1 || End[1] >= 1 && IsWinner[3] >= 1) || (Idle[0] >= 1 && FreePositions[0] >= 1 || Idle[1] >= 1 && FreePositions[0] >= 1 || Idle[0] >= 1 && FreePositions[4] >= 1 || Idle[1] >= 1 && FreePositions[4] >= 1 || Idle[0] >= 1 && FreePositions[2] >= 1 || Idle[1] >= 1 && FreePositions[2] >= 1 || Idle[0] >= 1 && FreePositions[6] >= 1 || Idle[1] >= 1 && FreePositions[6] >= 1 || Idle[0] >= 1 && FreePositions[1] >= 1 || Idle[1] >= 1 && FreePositions[1] >= 1 || Idle[0] >= 1 && FreePositions[5] >= 1 || Idle[1] >= 1 && FreePositions[5] >= 1 || Idle[0] >= 1 && FreePositions[3] >= 1 || Idle[1] >= 1 && FreePositions[3] >= 1 || Idle[0] >= 1 && FreePositions[7] >= 1 || Idle[1] >= 1 && FreePositions[7] >= 1)
Read property : p_48_fireability_and with value :(Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1) && (Eval1[2] >= 1 && FreePositions[0] >= 1 || Eval1[10] >= 1 && FreePositions[0] >= 1 || Eval1[2] >= 1 && FreePositions[4] >= 1 || Eval1[10] >= 1 && FreePositions[4] >= 1 || Eval1[2] >= 1 && FreePositions[5] >= 1 || Eval1[10] >= 1 && FreePositions[5] >= 1 || Eval1[5] >= 1 && FreePositions[0] >= 1 || Eval1[5] >= 1 && FreePositions[2] >= 1 || Eval1[13] >= 1 && FreePositions[0] >= 1 || Eval1[13] >= 1 && FreePositions[2] >= 1 || Eval1[5] >= 1 && FreePositions[4] >= 1 || Eval1[13] >= 1 && FreePositions[4] >= 1)
Read property : p_49_fireability_or with value :Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || (Eval1[2] >= 1 && FreePositions[0] >= 1 || Eval1[10] >= 1 && FreePositions[0] >= 1 || Eval1[2] >= 1 && FreePositions[4] >= 1 || Eval1[10] >= 1 && FreePositions[4] >= 1 || Eval1[2] >= 1 && FreePositions[5] >= 1 || Eval1[10] >= 1 && FreePositions[5] >= 1 || Eval1[5] >= 1 && FreePositions[0] >= 1 || Eval1[5] >= 1 && FreePositions[2] >= 1 || Eval1[13] >= 1 && FreePositions[0] >= 1 || Eval1[13] >= 1 && FreePositions[2] >= 1 || Eval1[5] >= 1 && FreePositions[4] >= 1 || Eval1[13] >= 1 && FreePositions[4] >= 1)
Read property : p_50_fireability_and_notx with value :! (Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[0] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[2] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[0] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[2] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[0] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[5] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[1] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[6] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[2] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[7] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[3] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[8] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[1] >= 1 && IsWinner[1] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[9] >= 1 && IsWinner[3] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[5] >= 1 && IsWinner[1] >= 1 && Score[4] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1 || Eval1[13] >= 1 && IsWinner[3] >= 1 && Score[9] >= 1 && OccupiedPositions[0] >= 1 && OccupiedPositions[2] >= 1 && OccupiedPositions[4] >= 1) && ! (Eval1[2] >= 1 && FreePositions[0] >= 1 || Eval1[10] >= 1 && FreePositions[0] >= 1 || Eval1[2] >= 1 && FreePositions[4] >= 1 || Eval1[10] >= 1 && FreePositions[4] >= 1 || Eval1[2] >= 1 && FreePositions[5] >= 1 || Eval1[10] >= 1 && FreePositions[5] >= 1 || Eval1[5] >= 1 && FreePositions[0] >= 1 || Eval1[5] >= 1 && FreePositions[2] >= 1 || Eval1[13] >= 1 && FreePositions[0] >= 1 || Eval1[13] >= 1 && FreePositions[2] >= 1 || Eval1[5] >= 1 && FreePositions[4] >= 1 || Eval1[13] >= 1 && FreePositions[4] >= 1)

--------------------
content from /tmp/BenchKit_head_log_file.1753: