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

------ Parsing...successful


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

Gamma_0: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]

Gamma_1: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))

Gamma_2: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]

Gamma_3: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]

Gamma_4: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]

Gamma_5: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))

Gamma_6: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]

Gamma_7: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))

Gamma_8: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]

Gamma_9: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]

Gamma_10: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))

Gamma_11: (extend-no-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  11: ~(succeeds(p8,p3)), ~(succeeds(p3,p8)), [succeeds(p3,p3)]

Gamma_12: (extend-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  11: ~(succeeds(p8,p3)), ~(succeeds(p3,p8)), [succeeds(p3,p3)]
  12: [~(succeeds(p3,p3))]

Gamma_13: (move)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  11: [~(succeeds(p3,p3))]
  12: ~(succeeds(p8,p3)), ~(succeeds(p3,p8)), [succeeds(p3,p3)]

Gamma_14: (resolve)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  11: [~(succeeds(p3,p3))]
  12: [~(succeeds(p8,p3))], ~(succeeds(p3,p8))

Gamma_15: (extend-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  11: [~(succeeds(p3,p3))]
  12: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]

Gamma_16: (move)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  11: [succeeds(p3,p8)], ~(has(p8,goto(loop))), ~(labels(loop,p3))
  12: [~(succeeds(p3,p3))]

Gamma_17: (resolve)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  11: ~(succeeds(p8,p3)), [~(has(p8,goto(loop)))], ~(labels(loop,p3))
  12: [~(succeeds(p3,p3))]

Gamma_18: (extend-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: [labels(loop,p3)]
  10: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  11: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  12: [~(succeeds(p3,p3))]

Gamma_19: (move)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  10: [labels(loop,p3)]
  11: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  12: [~(succeeds(p3,p3))]

Gamma_20: (resolve)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  10: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  11: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  12: [~(succeeds(p3,p3))]

Gamma_21: (extend-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [succeeds(p8,p3)], ~(follows(p8,p3))
  6: [follows(p5,p4)]
  7: [succeeds(p5,p4)], ~(follows(p5,p4))
  8: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  9: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  10: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  11: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  12: [~(succeeds(p3,p3))]

Gamma_22: (move)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  6: [succeeds(p8,p3)], ~(follows(p8,p3))
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: ~(succeeds(p8,p3)), ~(has(p8,goto(loop))), [~(labels(loop,p3))]
  11: ~(succeeds(p8,p3)), [~(succeeds(p3,p8))]
  12: [~(succeeds(p3,p3))]

Gamma_23: (resolve)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  6: ~(has(p8,goto(loop))), [~(follows(p8,p3))]
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: [~(succeeds(p3,p3))]

Gamma_24: (extend-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: [follows(p8,p3)]
  5: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  6: ~(has(p8,goto(loop))), [~(follows(p8,p3))]
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: [~(succeeds(p3,p3))]

Gamma_25: (move)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: ~(has(p8,goto(loop))), [~(follows(p8,p3))]
  5: [follows(p8,p3)]
  6: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: [~(succeeds(p3,p3))]

Gamma_26: (resolve)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: ~(has(p8,goto(loop))), [~(follows(p8,p3))]
  5: [~(has(p8,goto(loop)))]
  6: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: [~(succeeds(p3,p3))]

Gamma_27: (extend-conflict)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [has(p8,goto(loop))]
  3: [has(p4,goto(out))]
  4: ~(has(p8,goto(loop))), [~(follows(p8,p3))]
  5: [~(has(p8,goto(loop)))]
  6: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: [~(succeeds(p3,p3))]

Gamma_28: (move)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [~(has(p8,goto(loop)))]
  3: [has(p8,goto(loop))]
  4: [has(p4,goto(out))]
  5: ~(has(p8,goto(loop))), [~(follows(p8,p3))]
  6: [~(succeeds(p8,p3))], ~(has(p8,goto(loop)))
  7: [follows(p5,p4)]
  8: [succeeds(p5,p4)], ~(follows(p5,p4))
  9: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  10: [~(succeeds(p3,p3))]

Gamma_29: (resolve)
  0: [has(p3,ifthen(equal_function(register_j,n),p4))]
  1: [succeeds(p4,p3)], ~(has(p3,ifthen(equal_function(register_j,n),p4)))
  2: [~(has(p8,goto(loop)))]
  3: []
  4: [has(p4,goto(out))]
  5: [follows(p5,p4)]
  6: [succeeds(p5,p4)], ~(follows(p5,p4))
  7: ~(succeeds(p4,p3)), ~(succeeds(p5,p4)), [succeeds(p5,p3)]
  8: [~(succeeds(p3,p3))]

SZS status Unsatisfiable