{"action":"opened","issue":{"url":"https://api.github.com/repos/gilith/metis/issues/7","repository_url":"https://api.github.com/repos/gilith/metis","labels_url":"https://api.github.com/repos/gilith/metis/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/gilith/metis/issues/7/comments","events_url":"https://api.github.com/repos/gilith/metis/issues/7/events","html_url":"https://github.com/gilith/metis/issues/7","id":265652523,"number":7,"title":"[ BUG ] Simplify erroneously deduces $false","user":{"login":"jonaprieto","id":1428088,"avatar_url":"https://avatars2.githubusercontent.com/u/1428088?v=4","gravatar_id":"","url":"https://api.github.com/users/jonaprieto","html_url":"https://github.com/jonaprieto","followers_url":"https://api.github.com/users/jonaprieto/followers","following_url":"https://api.github.com/users/jonaprieto/following{/other_user}","gists_url":"https://api.github.com/users/jonaprieto/gists{/gist_id}","starred_url":"https://api.github.com/users/jonaprieto/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonaprieto/subscriptions","organizations_url":"https://api.github.com/users/jonaprieto/orgs","repos_url":"https://api.github.com/users/jonaprieto/repos","events_url":"https://api.github.com/users/jonaprieto/events{/privacy}","received_events_url":"https://api.github.com/users/jonaprieto/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-10-16T05:43:27Z","updated_at":"2017-10-16T05:43:27Z","closed_at":null,"author_association":"NONE","body":"Hi Joe,\r\n\r\nConsider the following problem:\r\n\r\n```\r\n$ cat conj-01.tptp\r\nfof(a1, axiom, p).\r\nfof(a2, axiom, q).\r\nfof(goal, conjecture, p & q).\r\n$ metis --version\r\nmetis 2.3 (release 20171005)\r\n$ metis --show proof conj-01.tptp\r\n...\r\nfof(a1, axiom, (p)).\r\n\r\nfof(a2, axiom, (q)).\r\n...\r\nfof(normalize_0_0, plain, (~ p),\r\n    inference(canonicalize, [], [negate_0_0])).\r\n...\r\n\r\nfof(normalize_1_0, plain, (~ q & p),\r\n    inference(canonicalize, [], [negate_1_0])).\r\n\r\nfof(normalize_1_1, plain, (q), inference(canonicalize, [], [a2])).\r\n\r\nfof(normalize_1_2, plain, (p), inference(canonicalize, [], [a1])).\r\n\r\nfof(normalize_1_3, plain, ($false),\r\n    inference(simplify, [],\r\n              [normalize_1_0, normalize_1_1, normalize_1_2])).\r\n\r\ncnf(refute_1_0, plain, ($false),\r\n    inference(canonicalize, [], [normalize_1_3])).\r\n% SZS output end CNFRefutation for conj-01.tptp \r\n```\r\n\r\nInstead of using normalize_1_2, Metis should use for example normalize_0_0 to deduce $false in this example.\r\n\r\nCC'ing @asr "}}
{"actor":{"display_login":"jonaprieto"}}