%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)] Gamma_1: (extend-no-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) Gamma_2: (extend-no-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg)] Gamma_3: (extend-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg)] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_4: (move) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] 3: ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg)] Gamma_5: (resolve) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_6: (extend-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_7: (move) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 2: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_8: (resolve) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_9: (extend-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_10: (move) 0: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_11: (resolve) 0: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 1: [] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)] Gamma_1: (extend-no-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) Gamma_2: (extend-no-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB), c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg)] Gamma_3: (extend-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg)] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_4: (move) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] 3: ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)), [c_in( c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg)] Gamma_5: (resolve) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_6: (extend-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] Gamma_7: (move) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 2: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)], ~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg)) 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_8: (resolve) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_9: (extend-conflict) 0: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 1: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_10: (move) 0: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 1: [c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)), tc_Message_Omsg)] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] Gamma_11: (resolve) 0: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oanalz(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 1: [] 2: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Message_Oparts(c_Event_Oknows(c_Message_Oagent_OSpy,v_evs2)),tc_Message_Omsg))] 3: [~(c_in(c_Message_Omsg_ONonce(v_NB),c_Event_Oused(v_evs2),tc_Message_Omsg))] SZS status Unsatisfiable