Number of relations: 1168
Number of variables: 96
Number of target variables: 96
Number of known variables: 32
Number of guessed variables: 6
Number of state copies (max_steps): 20
An upper bound for the number of guessed variables given by user (max_guess): 6
96 out of 96 state variables are known after 20 state copies
############################################################
The following 6 variable(s) are guessed:
X_0_1_3, X_0_2_0, K_1_0_3, W_0_1_2, W_0_2_2, K_1_3_3
############################################################
The following 32 variable(s) are initially known:
P_0_0, P_0_1, P_0_2, P_0_3, P_1_0, P_1_1, P_1_2, P_1_3, P_2_0, P_2_1, P_2_2, P_2_3, P_3_0, P_3_1, P_3_2, P_3_3, X_1_0_0, X_1_0_1, X_1_0_2, X_1_0_3, X_1_1_0, X_1_1_1, X_1_1_2, X_1_1_3, X_1_2_0, X_1_2_1, X_1_2_2, X_1_2_3, X_1_3_0, X_1_3_1, X_1_3_2, X_1_3_3
############################################################
Target variables:
P_0_0, K_0_0_0, X_0_0_0, P_0_1, K_0_0_1, X_0_0_1, P_0_2, K_0_0_2, X_0_0_2, P_0_3, K_0_0_3, X_0_0_3, P_1_0, K_0_1_0, X_0_1_0, P_1_1, K_0_1_1, X_0_1_1, P_1_2, K_0_1_2, X_0_1_2, P_1_3, K_0_1_3, X_0_1_3, P_2_0, K_0_2_0, X_0_2_0, P_2_1, K_0_2_1, X_0_2_1, P_2_2, K_0_2_2, X_0_2_2, P_2_3, K_0_2_3, X_0_2_3, P_3_0, K_0_3_0, X_0_3_0, P_3_1, K_0_3_1, X_0_3_1, P_3_2, K_0_3_2, X_0_3_2, P_3_3, K_0_3_3, X_0_3_3, W_0_0_0, K_1_0_0, X_1_0_0, W_0_0_1, K_1_0_1, X_1_0_1, W_0_0_2, K_1_0_2, X_1_0_2, W_0_0_3, K_1_0_3, X_1_0_3, W_0_1_0, K_1_1_0, X_1_1_0, W_0_1_1, K_1_1_1, X_1_1_1, W_0_1_2, K_1_1_2, X_1_1_2, W_0_1_3, K_1_1_3, X_1_1_3, W_0_2_0, K_1_2_0, X_1_2_0, W_0_2_1, K_1_2_1, X_1_2_1, W_0_2_2, K_1_2_2, X_1_2_2, W_0_2_3, K_1_2_3, X_1_2_3, W_0_3_0, K_1_3_0, X_1_3_0, W_0_3_1, K_1_3_1, X_1_3_1, W_0_3_2, K_1_3_2, X_1_3_2, W_0_3_3, K_1_3_3, X_1_3_3
############################################################
Determination flow:

State 0:
P_1_3, X_0_1_3 in symmetric relation [P_1_3, K_0_1_3, X_0_1_3] are known: P_1_3, X_0_1_3 ===> K_0_1_3
P_2_0, X_0_2_0 in symmetric relation [P_2_0, K_0_2_0, X_0_2_0] are known: P_2_0, X_0_2_0 ===> K_0_2_0
K_1_0_3, X_1_0_3 in symmetric relation [W_0_0_3, K_1_0_3, X_1_0_3] are known: K_1_0_3, X_1_0_3 ===> W_0_0_3
W_0_1_2, X_1_1_2 in symmetric relation [W_0_1_2, K_1_1_2, X_1_1_2] are known: W_0_1_2, X_1_1_2 ===> K_1_1_2
W_0_2_2, X_1_2_2 in symmetric relation [W_0_2_2, K_1_2_2, X_1_2_2] are known: W_0_2_2, X_1_2_2 ===> K_1_2_2
K_1_3_3, X_1_3_3 in symmetric relation [W_0_3_3, K_1_3_3, X_1_3_3] are known: K_1_3_3, X_1_3_3 ===> W_0_3_3
X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 in implication relation [X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2, X_0_0_2] are known: X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 ===> X_0_0_2
X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 in implication relation [X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2, X_0_3_1] are known: X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 ===> X_0_3_1
X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 in implication relation [X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2, W_0_0_2] are known: X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 ===> W_0_0_2
X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 in implication relation [X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2, W_0_3_2] are known: X_0_1_3, X_0_2_0, W_0_1_2, W_0_2_2 ===> W_0_3_2
############################################################
State 1:
P_0_2, X_0_0_2 in symmetric relation [P_0_2, K_0_0_2, X_0_0_2] are known: P_0_2, X_0_0_2 ===> K_0_0_2
P_3_1, X_0_3_1 in symmetric relation [P_3_1, K_0_3_1, X_0_3_1] are known: P_3_1, X_0_3_1 ===> K_0_3_1
W_0_0_2, X_1_0_2 in symmetric relation [W_0_0_2, K_1_0_2, X_1_0_2] are known: W_0_0_2, X_1_0_2 ===> K_1_0_2
W_0_3_2, X_1_3_2 in symmetric relation [W_0_3_2, K_1_3_2, X_1_3_2] are known: W_0_3_2, X_1_3_2 ===> K_1_3_2
K_0_1_3, K_1_1_2 in symmetric relation [K_0_1_3, K_1_1_2, K_1_1_3] are known: K_0_1_3, K_1_1_2 ===> K_1_1_3
############################################################
State 2:
K_1_1_3, X_1_1_3 in symmetric relation [W_0_1_3, K_1_1_3, X_1_1_3] are known: K_1_1_3, X_1_1_3 ===> W_0_1_3
K_1_3_2, K_1_3_3 in symmetric relation [K_0_3_3, K_1_3_2, K_1_3_3] are known: K_1_3_2, K_1_3_3 ===> K_0_3_3
K_1_0_2, K_1_0_3 in symmetric relation [K_0_0_3, K_1_0_2, K_1_0_3] are known: K_1_0_2, K_1_0_3 ===> K_0_0_3
K_0_0_2, K_1_0_2 in symmetric relation [K_0_0_2, K_1_0_1, K_1_0_2] are known: K_0_0_2, K_1_0_2 ===> K_1_0_1
############################################################
State 3:
P_0_3, K_0_0_3 in symmetric relation [P_0_3, K_0_0_3, X_0_0_3] are known: P_0_3, K_0_0_3 ===> X_0_0_3
P_3_3, K_0_3_3 in symmetric relation [P_3_3, K_0_3_3, X_0_3_3] are known: P_3_3, K_0_3_3 ===> X_0_3_3
K_1_0_1, X_1_0_1 in symmetric relation [W_0_0_1, K_1_0_1, X_1_0_1] are known: K_1_0_1, X_1_0_1 ===> W_0_0_1
K_0_2_0, K_0_3_3 in symmetric relation [K_0_2_0, K_0_3_3, K_1_2_0] are known: K_0_2_0, K_0_3_3 ===> K_1_2_0
############################################################
State 4:
K_1_2_0, X_1_2_0 in symmetric relation [W_0_2_0, K_1_2_0, X_1_2_0] are known: K_1_2_0, X_1_2_0 ===> W_0_2_0
X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 in implication relation [X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3, X_0_1_0] are known: X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 ===> X_0_1_0
X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 in implication relation [X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3, X_0_2_1] are known: X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 ===> X_0_2_1
X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 in implication relation [X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3, X_0_3_2] are known: X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 ===> X_0_3_2
X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 in implication relation [X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3, W_0_2_3] are known: X_0_0_3, W_0_0_3, W_0_1_3, W_0_3_3 ===> W_0_2_3
############################################################
State 5:
P_1_0, X_0_1_0 in symmetric relation [P_1_0, K_0_1_0, X_0_1_0] are known: P_1_0, X_0_1_0 ===> K_0_1_0
P_2_1, X_0_2_1 in symmetric relation [P_2_1, K_0_2_1, X_0_2_1] are known: P_2_1, X_0_2_1 ===> K_0_2_1
P_3_2, X_0_3_2 in symmetric relation [P_3_2, K_0_3_2, X_0_3_2] are known: P_3_2, X_0_3_2 ===> K_0_3_2
W_0_2_3, X_1_2_3 in symmetric relation [W_0_2_3, K_1_2_3, X_1_2_3] are known: W_0_2_3, X_1_2_3 ===> K_1_2_3
############################################################
State 6:
K_0_3_2, K_1_3_2 in symmetric relation [K_0_3_2, K_1_3_1, K_1_3_2] are known: K_0_3_2, K_1_3_2 ===> K_1_3_1
K_1_2_2, K_1_2_3 in symmetric relation [K_0_2_3, K_1_2_2, K_1_2_3] are known: K_1_2_2, K_1_2_3 ===> K_0_2_3
K_0_2_1, K_1_2_0 in symmetric relation [K_0_2_1, K_1_2_0, K_1_2_1] are known: K_0_2_1, K_1_2_0 ===> K_1_2_1
############################################################
State 7:
P_2_3, K_0_2_3 in symmetric relation [P_2_3, K_0_2_3, X_0_2_3] are known: P_2_3, K_0_2_3 ===> X_0_2_3
K_1_2_1, X_1_2_1 in symmetric relation [W_0_2_1, K_1_2_1, X_1_2_1] are known: K_1_2_1, X_1_2_1 ===> W_0_2_1
K_1_3_1, X_1_3_1 in symmetric relation [W_0_3_1, K_1_3_1, X_1_3_1] are known: K_1_3_1, X_1_3_1 ===> W_0_3_1
K_0_3_1, K_1_3_1 in symmetric relation [K_0_3_1, K_1_3_0, K_1_3_1] are known: K_0_3_1, K_1_3_1 ===> K_1_3_0
K_1_2_1, K_1_2_2 in symmetric relation [K_0_2_2, K_1_2_1, K_1_2_2] are known: K_1_2_1, K_1_2_2 ===> K_0_2_2
K_0_1_0, K_0_2_3 in symmetric relation [K_0_1_0, K_0_2_3, K_1_1_0] are known: K_0_1_0, K_0_2_3 ===> K_1_1_0
############################################################
State 8:
P_2_2, K_0_2_2 in symmetric relation [P_2_2, K_0_2_2, X_0_2_2] are known: P_2_2, K_0_2_2 ===> X_0_2_2
K_1_1_0, X_1_1_0 in symmetric relation [W_0_1_0, K_1_1_0, X_1_1_0] are known: K_1_1_0, X_1_1_0 ===> W_0_1_0
K_1_3_0, X_1_3_0 in symmetric relation [W_0_3_0, K_1_3_0, X_1_3_0] are known: K_1_3_0, X_1_3_0 ===> W_0_3_0
K_0_0_3, K_1_3_0 in symmetric relation [K_0_0_3, K_0_3_0, K_1_3_0] are known: K_0_0_3, K_1_3_0 ===> K_0_3_0
X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 in implication relation [X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1, X_0_0_1] are known: X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 ===> X_0_0_1
X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 in implication relation [X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1, X_0_1_2] are known: X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 ===> X_0_1_2
X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 in implication relation [X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1, X_0_3_0] are known: X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 ===> X_0_3_0
X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 in implication relation [X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1, W_0_1_1] are known: X_0_2_3, W_0_0_1, W_0_2_1, W_0_3_1 ===> W_0_1_1
############################################################
State 9:
P_0_1, X_0_0_1 in symmetric relation [P_0_1, K_0_0_1, X_0_0_1] are known: P_0_1, X_0_0_1 ===> K_0_0_1
P_1_2, X_0_1_2 in symmetric relation [P_1_2, K_0_1_2, X_0_1_2] are known: P_1_2, X_0_1_2 ===> K_0_1_2
W_0_1_1, X_1_1_1 in symmetric relation [W_0_1_1, K_1_1_1, X_1_1_1] are known: W_0_1_1, X_1_1_1 ===> K_1_1_1
X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0 in implication relation [X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0, X_0_0_0] are known: X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0 ===> X_0_0_0
X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0 in implication relation [X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0, X_0_1_1] are known: X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0 ===> X_0_1_1
X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0 in implication relation [X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0, W_0_0_0] are known: X_0_2_2, X_0_3_3, W_0_1_0, W_0_2_0 ===> W_0_0_0
X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0 in implication relation [X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0, X_0_0_0] are known: X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0 ===> X_0_0_0
X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0 in implication relation [X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0, X_0_1_1] are known: X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0 ===> X_0_1_1
X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0 in implication relation [X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0, W_0_0_0] are known: X_0_2_2, X_0_3_3, W_0_1_0, W_0_3_0 ===> W_0_0_0
X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0 in implication relation [X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0, X_0_0_0] are known: X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0 ===> X_0_0_0
X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0 in implication relation [X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0, X_0_1_1] are known: X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0 ===> X_0_1_1
X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0 in implication relation [X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0, W_0_0_0] are known: X_0_2_2, X_0_3_3, W_0_2_0, W_0_3_0 ===> W_0_0_0
X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0 in implication relation [X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0, X_0_0_0] are known: X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0 ===> X_0_0_0
X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0 in implication relation [X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0, X_0_1_1] are known: X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0 ===> X_0_1_1
X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0 in implication relation [X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0, W_0_0_0] are known: X_0_2_2, W_0_1_0, W_0_2_0, W_0_3_0 ===> W_0_0_0
X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0 in implication relation [X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0, X_0_0_0] are known: X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0 ===> X_0_0_0
X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0 in implication relation [X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0, X_0_1_1] are known: X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0 ===> X_0_1_1
X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0 in implication relation [X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0, W_0_0_0] are known: X_0_3_3, W_0_1_0, W_0_2_0, W_0_3_0 ===> W_0_0_0
############################################################
State 10:
P_0_0, X_0_0_0 in symmetric relation [P_0_0, K_0_0_0, X_0_0_0] are known: P_0_0, X_0_0_0 ===> K_0_0_0
P_1_1, X_0_1_1 in symmetric relation [P_1_1, K_0_1_1, X_0_1_1] are known: P_1_1, X_0_1_1 ===> K_0_1_1
W_0_0_0, X_1_0_0 in symmetric relation [W_0_0_0, K_1_0_0, X_1_0_0] are known: W_0_0_0, X_1_0_0 ===> K_1_0_0
K_1_1_0, K_1_1_1 in symmetric relation [K_0_1_1, K_1_1_0, K_1_1_1] are known: K_1_1_0, K_1_1_1 ===> K_0_1_1
K_0_0_1, K_1_0_1 in symmetric relation [K_0_0_1, K_1_0_0, K_1_0_1] are known: K_0_0_1, K_1_0_1 ===> K_1_0_0
############################################################
The following variables are known in final state:
P_0_0, K_0_0_0, X_0_0_0, P_0_1, K_0_0_1, X_0_0_1, P_0_2, K_0_0_2, X_0_0_2, P_0_3, K_0_0_3, X_0_0_3, P_1_0, K_0_1_0, X_0_1_0, P_1_1, K_0_1_1, X_0_1_1, P_1_2, K_0_1_2, X_0_1_2, P_1_3, K_0_1_3, X_0_1_3, P_2_0, K_0_2_0, X_0_2_0, P_2_1, K_0_2_1, X_0_2_1, P_2_2, K_0_2_2, X_0_2_2, P_2_3, K_0_2_3, X_0_2_3, P_3_0, K_0_3_0, X_0_3_0, P_3_1, K_0_3_1, X_0_3_1, P_3_2, K_0_3_2, X_0_3_2, P_3_3, K_0_3_3, X_0_3_3, W_0_0_0, K_1_0_0, X_1_0_0, W_0_0_1, K_1_0_1, X_1_0_1, W_0_0_2, K_1_0_2, X_1_0_2, W_0_0_3, K_1_0_3, X_1_0_3, W_0_1_0, K_1_1_0, X_1_1_0, W_0_1_1, K_1_1_1, X_1_1_1, W_0_1_2, K_1_1_2, X_1_1_2, W_0_1_3, K_1_1_3, X_1_1_3, W_0_2_0, K_1_2_0, X_1_2_0, W_0_2_1, K_1_2_1, X_1_2_1, W_0_2_2, K_1_2_2, X_1_2_2, W_0_2_3, K_1_2_3, X_1_2_3, W_0_3_0, K_1_3_0, X_1_3_0, W_0_3_1, K_1_3_1, X_1_3_1, W_0_3_2, K_1_3_2, X_1_3_2, W_0_3_3, K_1_3_3, X_1_3_3