%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [sym_q_0], sym_p_0

Gamma_1: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)

Gamma_2: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3

Gamma_3: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)

Gamma_4: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)
  4: [sym_q_4], ~(sym_q_2), sym_p_3

Gamma_5: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)
  4: [sym_q_4], ~(sym_q_2), sym_p_3
  5: ~(sym_q_1), [sym_q_3], sym_p_2
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)
  4: [sym_q_4], ~(sym_q_2), sym_p_3
  5: ~(sym_q_1), [sym_q_3], sym_p_2

SZS status Satisfiable

%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------%

------ Parsing...successful


------ Proving...
use I-

Gamma_0: (extend-no-conflict)
  0: [sym_q_0], sym_p_0

Gamma_1: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)

Gamma_2: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3

Gamma_3: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)

Gamma_4: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)
  4: [sym_q_4], ~(sym_q_2), sym_p_3

Gamma_5: (extend-no-conflict)
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)
  4: [sym_q_4], ~(sym_q_2), sym_p_3
  5: ~(sym_q_1), [sym_q_3], sym_p_2
  0: [sym_q_0], sym_p_0
  1: [sym_q_1], sym_p_2, ~(sym_q_0)
  2: ~(sym_q_1), [sym_q_2], sym_p_3
  3: [sym_p_4], sym_q_3, ~(sym_q_2)
  4: [sym_q_4], ~(sym_q_2), sym_p_3
  5: ~(sym_q_1), [sym_q_3], sym_p_2

SZS status Satisfiable