%---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [can_be_read] Gamma_1: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed Gamma_2: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) Gamma_3: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] Gamma_4: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [begins_with_dear_sir], ~(by_brown) Gamma_5: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [begins_with_dear_sir], ~(by_brown) 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_6: (move) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [~(begins_with_dear_sir)], ~(in_third_person) 5: [begins_with_dear_sir], ~(by_brown) Gamma_7: (resolve) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [~(begins_with_dear_sir)], ~(in_third_person) 5: ~(in_third_person), [~(by_brown)] Gamma_8: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [~(begins_with_dear_sir)], ~(in_third_person) 5: ~(in_third_person), [~(by_brown)] Gamma_9: (move) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: ~(in_third_person), [~(by_brown)] 4: [by_brown] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_10: (resolve) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: ~(in_third_person), [~(by_brown)] 4: [~(in_third_person)] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_11: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: ~(in_third_person), [~(by_brown)] 4: [~(in_third_person)] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_12: (move) 0: [can_be_read] 1: [in_black_ink], crossed 2: [~(in_third_person)] 3: [in_third_person], ~(in_black_ink) 4: ~(in_third_person), [~(by_brown)] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_13: (resolve) 0: [can_be_read] 1: [in_black_ink], crossed 2: [~(in_third_person)] 3: [~(in_black_ink)] Gamma_14: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [~(in_third_person)] 3: [~(in_black_ink)] Gamma_15: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [in_black_ink], crossed 3: [~(in_third_person)] Gamma_16: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] Gamma_17: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] Gamma_18: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) Gamma_19: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] Gamma_20: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] Gamma_21: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [filed], ~(on_blue_paper) Gamma_22: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [filed], ~(on_blue_paper) 8: [~(filed)], ~(can_be_read) Gamma_23: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [~(filed)], ~(can_be_read) 8: [filed], ~(on_blue_paper) Gamma_24: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [~(filed)], ~(can_be_read) 8: [~(on_blue_paper)], ~(can_be_read) Gamma_25: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [~(filed)], ~(can_be_read) 8: [~(on_blue_paper)], ~(can_be_read) Gamma_26: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: [~(on_blue_paper)], ~(can_be_read) 7: ~(dated), [on_blue_paper] 8: [~(filed)], ~(can_be_read) Gamma_27: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: [~(on_blue_paper)], ~(can_be_read) 7: [~(dated)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_28: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: [~(on_blue_paper)], ~(can_be_read) 7: [~(dated)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_29: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: [~(dated)], ~(can_be_read) 6: ~(on_one_sheet), [dated] 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_30: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: [~(dated)], ~(can_be_read) 6: [~(on_one_sheet)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_31: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: [~(dated)], ~(can_be_read) 6: [~(on_one_sheet)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_32: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [~(on_one_sheet)], ~(can_be_read) 5: [on_one_sheet], ~(crossed) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_33: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [~(on_one_sheet)], ~(can_be_read) 5: [~(crossed)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_34: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [~(on_one_sheet)], ~(can_be_read) 5: [~(crossed)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_35: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [~(crossed)], ~(can_be_read) 3: [crossed] 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_36: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [~(crossed)], ~(can_be_read) 3: [~(can_be_read)] 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_37: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [~(crossed)], ~(can_be_read) 3: [~(can_be_read)] 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_38: (move) 0: [~(can_be_read)] 1: [can_be_read] 2: [~(in_black_ink)] 3: [~(crossed)], ~(can_be_read) 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_39: (resolve) 0: [~(can_be_read)] 1: [] 2: [~(in_black_ink)] 3: [~(in_third_person)] SZS status Unsatisfiable %---------------- SGGS v1.0 (IJCAR 2020 submission) ----------------% ------ Parsing...successful ------ Proving... use I- Gamma_0: (extend-no-conflict) 0: [can_be_read] Gamma_1: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed Gamma_2: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) Gamma_3: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] Gamma_4: (extend-no-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [begins_with_dear_sir], ~(by_brown) Gamma_5: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [begins_with_dear_sir], ~(by_brown) 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_6: (move) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [~(begins_with_dear_sir)], ~(in_third_person) 5: [begins_with_dear_sir], ~(by_brown) Gamma_7: (resolve) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [~(begins_with_dear_sir)], ~(in_third_person) 5: ~(in_third_person), [~(by_brown)] Gamma_8: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: [by_brown] 4: [~(begins_with_dear_sir)], ~(in_third_person) 5: ~(in_third_person), [~(by_brown)] Gamma_9: (move) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: ~(in_third_person), [~(by_brown)] 4: [by_brown] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_10: (resolve) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: ~(in_third_person), [~(by_brown)] 4: [~(in_third_person)] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_11: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [in_third_person], ~(in_black_ink) 3: ~(in_third_person), [~(by_brown)] 4: [~(in_third_person)] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_12: (move) 0: [can_be_read] 1: [in_black_ink], crossed 2: [~(in_third_person)] 3: [in_third_person], ~(in_black_ink) 4: ~(in_third_person), [~(by_brown)] 5: [~(begins_with_dear_sir)], ~(in_third_person) Gamma_13: (resolve) 0: [can_be_read] 1: [in_black_ink], crossed 2: [~(in_third_person)] 3: [~(in_black_ink)] Gamma_14: (extend-conflict) 0: [can_be_read] 1: [in_black_ink], crossed 2: [~(in_third_person)] 3: [~(in_black_ink)] Gamma_15: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [in_black_ink], crossed 3: [~(in_third_person)] Gamma_16: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] Gamma_17: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] Gamma_18: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) Gamma_19: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] Gamma_20: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] Gamma_21: (extend-no-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [filed], ~(on_blue_paper) Gamma_22: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [filed], ~(on_blue_paper) 8: [~(filed)], ~(can_be_read) Gamma_23: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [~(filed)], ~(can_be_read) 8: [filed], ~(on_blue_paper) Gamma_24: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [~(filed)], ~(can_be_read) 8: [~(on_blue_paper)], ~(can_be_read) Gamma_25: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: ~(dated), [on_blue_paper] 7: [~(filed)], ~(can_be_read) 8: [~(on_blue_paper)], ~(can_be_read) Gamma_26: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: [~(on_blue_paper)], ~(can_be_read) 7: ~(dated), [on_blue_paper] 8: [~(filed)], ~(can_be_read) Gamma_27: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: [~(on_blue_paper)], ~(can_be_read) 7: [~(dated)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_28: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: ~(on_one_sheet), [dated] 6: [~(on_blue_paper)], ~(can_be_read) 7: [~(dated)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_29: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: [~(dated)], ~(can_be_read) 6: ~(on_one_sheet), [dated] 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_30: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: [~(dated)], ~(can_be_read) 6: [~(on_one_sheet)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_31: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [on_one_sheet], ~(crossed) 5: [~(dated)], ~(can_be_read) 6: [~(on_one_sheet)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_32: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [~(on_one_sheet)], ~(can_be_read) 5: [on_one_sheet], ~(crossed) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_33: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [~(on_one_sheet)], ~(can_be_read) 5: [~(crossed)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_34: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [crossed] 3: [~(in_third_person)] 4: [~(on_one_sheet)], ~(can_be_read) 5: [~(crossed)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_35: (move) 0: [can_be_read] 1: [~(in_black_ink)] 2: [~(crossed)], ~(can_be_read) 3: [crossed] 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_36: (resolve) 0: [can_be_read] 1: [~(in_black_ink)] 2: [~(crossed)], ~(can_be_read) 3: [~(can_be_read)] 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_37: (extend-conflict) 0: [can_be_read] 1: [~(in_black_ink)] 2: [~(crossed)], ~(can_be_read) 3: [~(can_be_read)] 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_38: (move) 0: [~(can_be_read)] 1: [can_be_read] 2: [~(in_black_ink)] 3: [~(crossed)], ~(can_be_read) 4: [~(in_third_person)] 5: [~(on_one_sheet)], ~(can_be_read) 6: [~(dated)], ~(can_be_read) 7: [~(on_blue_paper)], ~(can_be_read) 8: [~(filed)], ~(can_be_read) Gamma_39: (resolve) 0: [~(can_be_read)] 1: [] 2: [~(in_black_ink)] 3: [~(in_third_person)] SZS status Unsatisfiable