%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) Gamma_1: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) Gamma_2: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) Gamma_3: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) Gamma_4: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) Gamma_5: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) Gamma_6: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] Gamma_7: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_8: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_9: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) 8: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_10: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) 8: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), [~(big_g(d))], ~(big_f(c)) Gamma_11: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) 8: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] Gamma_12: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 7: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_13: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_14: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_15: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 6: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 7: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_16: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 6: ~(big_j(d)), ~(big_j(f)), [~(big_g(d))], ~(big_f(e)) Gamma_17: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] Gamma_18: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(f)), [big_f(e)], big_f(c) 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) Gamma_19: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)), big_f(c) 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) Gamma_20: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) Gamma_21: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_22: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_23: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) 8: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_24: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) 8: ~(big_j(d)), ~(big_j(f)), [~(big_g(d))], big_f(e), ~(big_f(c)) Gamma_25: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) 8: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] Gamma_26: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_27: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: [~(big_j(d))], ~(big_j(f)), ~(big_g(d)), big_f(e) 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_28: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(e)] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_29: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: [~(big_j(d))], ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_30: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_31: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_32: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) Gamma_33: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) Gamma_34: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] Gamma_35: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: [big_f(a)] Gamma_36: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: [big_f(a)] 7: [big_j(j)], ~(big_g(j)), ~(big_f(a)) Gamma_37: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: [big_f(a)] 7: [big_j(j)], ~(big_g(j)), ~(big_f(a)) 8: big_j(f), ~(big_g(f)), [~(big_f(a))] Gamma_38: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: [big_f(a)] 8: [big_j(j)], ~(big_g(j)), ~(big_f(a)) Gamma_39: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: [big_j(f)], ~(big_g(f)) Gamma_40: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: [big_j(f)], ~(big_g(f)) Gamma_41: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] Gamma_42: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] Gamma_43: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: [big_g(f)], big_f(e), big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 6: [big_g(b)] 7: big_j(f), ~(big_g(f)), [~(big_f(a))] Gamma_44: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] Gamma_45: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] Gamma_46: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) Gamma_47: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) Gamma_48: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] Gamma_49: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_50: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 10: [big_f(a)] Gamma_51: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 10: [big_f(a)] 11: [big_h(a)], ~(big_g(d)), ~(big_f(a)) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 10: [big_f(a)] 11: [big_h(a)], ~(big_g(d)), ~(big_f(a)) SZS status Satisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) Gamma_1: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) Gamma_2: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) Gamma_3: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) Gamma_4: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) Gamma_5: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) Gamma_6: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] Gamma_7: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_8: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_9: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) 8: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_10: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) 8: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), [~(big_g(d))], ~(big_f(c)) Gamma_11: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 7: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) 8: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] Gamma_12: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 7: ~(big_h(e)), ~(big_j(f)), [big_f(c)] 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_13: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_14: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 6: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_15: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 6: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 7: ~(big_h(e)), ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(c))] 8: ~(big_h(e)), [~(big_h(c))], ~(big_j(d)), ~(big_j(f)) Gamma_16: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 6: ~(big_j(d)), ~(big_j(f)), [~(big_g(d))], ~(big_f(e)) Gamma_17: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(f)), [big_f(e)], big_f(c) 5: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] Gamma_18: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(f)), [big_f(e)], big_f(c) 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) Gamma_19: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)), big_f(c) 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) Gamma_20: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) Gamma_21: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_22: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_23: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) 8: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_24: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) 8: ~(big_j(d)), ~(big_j(f)), [~(big_g(d))], big_f(e), ~(big_f(c)) Gamma_25: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 6: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) 8: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] Gamma_26: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(c)] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_27: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: [~(big_j(d))], ~(big_j(f)), ~(big_g(d)), big_f(e) 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_28: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [big_f(e)] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_29: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: [~(big_j(d))], ~(big_j(f)), ~(big_g(d)) 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_30: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 4: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 6: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_31: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: [big_j(f)], big_g(j), ~(big_g(f)), big_f(e) 5: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), [~(big_f(e))] 6: ~(big_j(d)), ~(big_j(f)), ~(big_g(d)), big_f(e), [~(big_f(c))] 7: [~(big_h(e))], ~(big_j(d)), ~(big_j(f)), ~(big_g(d)) 8: [~(big_h(c))], ~(big_j(d)), ~(big_j(f)), big_f(e) Gamma_32: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) Gamma_33: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) Gamma_34: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] Gamma_35: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: [big_f(a)] Gamma_36: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: [big_f(a)] 7: [big_j(j)], ~(big_g(j)), ~(big_f(a)) Gamma_37: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: [big_f(a)] 7: [big_j(j)], ~(big_g(j)), ~(big_f(a)) 8: big_j(f), ~(big_g(f)), [~(big_f(a))] Gamma_38: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: [big_f(a)] 8: [big_j(j)], ~(big_g(j)), ~(big_f(a)) Gamma_39: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: [big_j(f)], ~(big_g(f)) Gamma_40: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: [big_j(f)], ~(big_g(f)) Gamma_41: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] Gamma_42: (extend-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: [big_g(f)], big_f(e), big_f(c) 3: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 4: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 5: [big_g(b)] 6: big_j(f), ~(big_g(f)), [~(big_f(a))] 7: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] Gamma_43: (move) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: [big_g(f)], big_f(e), big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: ~(big_j(d)), [big_g(j)], ~(big_g(d)), ~(big_g(f)), big_f(e) 6: [big_g(b)] 7: big_j(f), ~(big_g(f)), [~(big_f(a))] Gamma_44: (resolve) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] Gamma_45: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] Gamma_46: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) Gamma_47: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) Gamma_48: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] Gamma_49: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) Gamma_50: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 10: [big_f(a)] Gamma_51: (extend-no-conflict) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 10: [big_f(a)] 11: [big_h(a)], ~(big_g(d)), ~(big_f(a)) 0: [big_g(d)], big_g(f), big_f(e) 1: [big_j(d)], big_g(j), ~(big_g(d)), big_f(e) 2: ~(big_j(d)), ~(big_g(d)), [~(big_g(f))] 3: ~(big_j(d)), ~(big_g(d)), [big_f(e)], big_f(c) 4: ~(big_j(d)), [~(big_j(f))], ~(big_g(d)) 5: [big_g(b)] 6: [big_j(b)], ~(big_g(b)), ~(big_f(e)) 7: [big_h(e)], ~(big_g(d)), ~(big_f(e)) 8: ~(big_h(e)), big_g(f), [big_f(c)] 9: [big_h(c)], ~(big_g(d)), ~(big_f(c)) 10: [big_f(a)] 11: [big_h(a)], ~(big_g(d)), ~(big_f(a)) SZS status Satisfiable