%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] Gamma_1: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] Gamma_2: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] Gamma_3: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) Gamma_4: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [has_elaborated_routines(sk1,sk2)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(efficient_producer(sk1)) Gamma_5: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [has_elaborated_routines(sk1,sk2)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(efficient_producer(sk1)) 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_6: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [~(has_elaborated_routines(sk1,sk2))] 5: [has_elaborated_routines(sk1,sk2)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(efficient_producer(sk1)) Gamma_7: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(founding_time(sk1,sk2))], ~(organisation_at_time(sk1,sk2)), ~( efficient_producer(sk1)) Gamma_8: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [~(has_elaborated_routines(sk1,sk2))] 5: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] Gamma_9: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_10: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), [~(organisation_at_time(sk1,sk2))], first_mover( sk1) 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_11: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_12: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [number_of_routines(sk1,sk2,low)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) Gamma_13: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [number_of_routines(sk1,sk2,low)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_14: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) 7: [number_of_routines(sk1,sk2,low)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) Gamma_15: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) 7: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))], ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) Gamma_16: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) 7: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] Gamma_17: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 5: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_18: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 5: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))], ~( organisation_at_time(sk1,sk2)) 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_19: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 5: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_20: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 3: [organisation_at_time(sk1,sk2)] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 5: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_21: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 3: [~(number_of_routines(sk1,sk2,high))], ~(founding_time(sk1,sk2)) 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_22: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 3: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_23: (move) 0: [number_of_routines(sk1,sk2,high)] 1: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 2: [founding_time(sk1,sk2)] 3: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_24: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 2: [~(number_of_routines(sk1,sk2,high))] 3: [~(has_elaborated_routines(sk1,sk2))] 4: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_25: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 2: [~(number_of_routines(sk1,sk2,high))] 3: [~(has_elaborated_routines(sk1,sk2))] 4: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_26: (move) 0: [~(number_of_routines(sk1,sk2,high))] 1: [number_of_routines(sk1,sk2,high)] 2: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 3: [~(has_elaborated_routines(sk1,sk2))] 4: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_27: (resolve) 0: [~(number_of_routines(sk1,sk2,high))] 1: [] 2: [~(has_elaborated_routines(sk1,sk2))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] Gamma_1: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] Gamma_2: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] Gamma_3: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) Gamma_4: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [has_elaborated_routines(sk1,sk2)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(efficient_producer(sk1)) Gamma_5: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [has_elaborated_routines(sk1,sk2)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(efficient_producer(sk1)) 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_6: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [~(has_elaborated_routines(sk1,sk2))] 5: [has_elaborated_routines(sk1,sk2)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(efficient_producer(sk1)) Gamma_7: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(founding_time(sk1,sk2))], ~(organisation_at_time(sk1,sk2)), ~( efficient_producer(sk1)) Gamma_8: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 4: [~(has_elaborated_routines(sk1,sk2))] 5: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] Gamma_9: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(organisation_at_time(sk1,sk2)), [efficient_producer(sk1)], first_mover( sk1) 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_10: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), [~(organisation_at_time(sk1,sk2))], first_mover( sk1) 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_11: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] Gamma_12: (extend-no-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [number_of_routines(sk1,sk2,low)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) Gamma_13: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [number_of_routines(sk1,sk2,low)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_14: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) 7: [number_of_routines(sk1,sk2,low)], ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) Gamma_15: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) 7: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))], ~( organisation_at_time(sk1,sk2)), ~(first_mover(sk1)) Gamma_16: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 5: [~(has_elaborated_routines(sk1,sk2))] 6: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) 7: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] Gamma_17: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 5: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [first_mover( sk1)] 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_18: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 5: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))], ~( organisation_at_time(sk1,sk2)) 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_19: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: [organisation_at_time(sk1,sk2)] 3: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 4: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 5: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_20: (move) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 3: [organisation_at_time(sk1,sk2)] 4: ~(founding_time(sk1,sk2)), ~(organisation_at_time(sk1,sk2)), [~( efficient_producer(sk1))] 5: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), ~( organisation_at_time(sk1,sk2)), [~(first_mover(sk1))] 6: [~(has_elaborated_routines(sk1,sk2))] 7: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_21: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 3: [~(number_of_routines(sk1,sk2,high))], ~(founding_time(sk1,sk2)) 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_22: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: [founding_time(sk1,sk2)] 2: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 3: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_23: (move) 0: [number_of_routines(sk1,sk2,high)] 1: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 2: [founding_time(sk1,sk2)] 3: ~(number_of_routines(sk1,sk2,high)), ~(founding_time(sk1,sk2)), [~( organisation_at_time(sk1,sk2))] 4: [~(has_elaborated_routines(sk1,sk2))] 5: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_24: (resolve) 0: [number_of_routines(sk1,sk2,high)] 1: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 2: [~(number_of_routines(sk1,sk2,high))] 3: [~(has_elaborated_routines(sk1,sk2))] 4: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_25: (extend-conflict) 0: [number_of_routines(sk1,sk2,high)] 1: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 2: [~(number_of_routines(sk1,sk2,high))] 3: [~(has_elaborated_routines(sk1,sk2))] 4: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_26: (move) 0: [~(number_of_routines(sk1,sk2,high))] 1: [number_of_routines(sk1,sk2,high)] 2: ~(number_of_routines(sk1,sk2,high)), [~(founding_time(sk1,sk2))] 3: [~(has_elaborated_routines(sk1,sk2))] 4: [~(number_of_routines(sk1,sk2,low))], ~(number_of_routines(sk1,sk2,high)) Gamma_27: (resolve) 0: [~(number_of_routines(sk1,sk2,high))] 1: [] 2: [~(has_elaborated_routines(sk1,sk2))] SZS status Unsatisfiable