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