%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) Gamma_1: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) Gamma_2: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) Gamma_3: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) Gamma_4: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) Gamma_5: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) Gamma_6: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) Gamma_7: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) Gamma_8: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) Gamma_9: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) Gamma_10: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 10: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) Gamma_11: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 10: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 11: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) Gamma_12: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 10: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 11: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 12: [member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)], ~(shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)), actual_world(esk1_0) Gamma_13: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 10: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 11: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 12: [member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)], ~(shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)), actual_world(esk1_0) 13: ~(member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) Gamma_14: (extend-no-conflict) 0: [male(esk10_0,esk11_0)], male(esk1_0, esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 10: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 11: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 12: [member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)], ~(shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)), actual_world(esk1_0) 13: ~(member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 14: ~(member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 0: [male(esk10_0,esk11_0)], male(esk1_0,esk2_0) 1: [male(esk1_0,esk2_0)], six(esk10_0,esk12_0) 2: [six(esk10_0,esk12_0)], six(esk1_0,esk3_0) 3: [six(esk1_0,esk3_0)], group(esk10_0,esk12_0) 4: [group(esk10_0,esk12_0)], group(esk1_0,esk3_0) 5: [group(esk1_0,esk3_0)], actual_world(esk10_0) 6: [actual_world(esk10_0)], actual_world(esk1_0) 7: [member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)], member( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0), member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0), esk12_0), member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)) 8: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)], member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0), esk12_0), shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 9: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [member( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)], man(esk10_0,esk7_3(esk10_0,esk11_0,esk12_0)), shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0)), ~(male(esk10_0,esk11_0)), ~( six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~(actual_world(esk10_0)) 10: ~(member(esk10_0,esk8_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk8_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 11: ~(member(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 12: [member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)], ~(shot(esk10_0,esk16_3(esk10_0,esk11_0,esk12_0))), ~( male(esk10_0,esk11_0)), ~(six(esk10_0,esk12_0)), ~(group(esk10_0,esk12_0)), ~( actual_world(esk10_0)), actual_world(esk1_0) 13: ~(member(esk10_0,esk15_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk15_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) 14: ~(member(esk10_0,esk9_3(esk10_0,esk11_0,esk12_0),esk12_0)), [shot( esk10_0,esk9_3(esk10_0,esk11_0,esk12_0))], actual_world(esk1_0) SZS status Satisfiable