{"action":"created","issue":{"url":"https://api.github.com/repos/gapt/gapt/issues/384","labels_url":"https://api.github.com/repos/gapt/gapt/issues/384/labels{/name}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/384/comments","events_url":"https://api.github.com/repos/gapt/gapt/issues/384/events","html_url":"https://github.com/gapt/gapt/issues/384","id":107140193,"number":384,"title":"Duplicates edges in weak quantifier nodes in expansion trees","user":{"login":"gebner","id":313929,"avatar_url":"https://avatars.githubusercontent.com/u/313929?v=3","gravatar_id":"","url":"https://api.github.com/users/gebner","html_url":"https://github.com/gebner","followers_url":"https://api.github.com/users/gebner/followers","following_url":"https://api.github.com/users/gebner/following{/other_user}","gists_url":"https://api.github.com/users/gebner/gists{/gist_id}","starred_url":"https://api.github.com/users/gebner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gebner/subscriptions","organizations_url":"https://api.github.com/users/gebner/orgs","repos_url":"https://api.github.com/users/gebner/repos","events_url":"https://api.github.com/users/gebner/events{/privacy}","received_events_url":"https://api.github.com/users/gebner/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/gapt/gapt/labels/Bug","name":"Bug","color":"e11d21"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-09-18T06:13:48Z","updated_at":"2015-09-18T08:26:47Z","closed_at":null,"body":"Looking through the CSV file listing the non-trivial termsets of the prover9 import, the termset sizes usually change by a few terms every time we generate them.\r\n\r\nAfter the recent switch to the new resolution calculus, there are 221 proofs that have smaller term sets now, among those this is a fairly interesting one where the termset size almost halved compared to two weeks ago:\r\n```\r\nfile         LCL090-1\r\nnfuns_old           3\r\nterms_old        1745\r\nnfuns_new           3\r\nterms_new        1019\r\n```\r\n\r\n(Looking at the older lists as well, we have always obtained 1745 or 1746 terms for this proof.)\r\n\r\nInvesting a bit turned up a weird situation:\r\n```scala\r\nval expansion = Prover9Importer.expansionProofFromFile(\"testing/TSTP/prover9/LCL/LCL090-1/Prover9---1109a.UNS-Ref.s.out\")\r\nprintln(extractInstances(expansion).size)\r\nprintln(extractInstances(expansion).distinct.size)\r\nprintln(new InstanceTermEncoding(toShallow(expansion)).encode(expansion).distinct.size)\r\nprintln(new VeriTProver().isValid(extractInstances(expansion)))\r\n```\r\nprints\r\n```\r\n1572\r\n1019\r\n1019\r\ntrue\r\n```\r\n\r\nI.e. `extractInstances` returns many duplicate instances.  This seems to happen because the ETWeakQuantifier node contains duplicate edges.  The expansion trees are generated by `formulaToExpansionTree`.\r\n\r\n(ETWeakQuantifier doesn't do any kind of validation at the moment.)"},"comment":{"url":"https://api.github.com/repos/gapt/gapt/issues/comments/141380200","html_url":"https://github.com/gapt/gapt/issues/384#issuecomment-141380200","issue_url":"https://api.github.com/repos/gapt/gapt/issues/384","id":141380200,"user":{"login":"gebner","id":313929,"avatar_url":"https://avatars.githubusercontent.com/u/313929?v=3","gravatar_id":"","url":"https://api.github.com/users/gebner","html_url":"https://github.com/gebner","followers_url":"https://api.github.com/users/gebner/followers","following_url":"https://api.github.com/users/gebner/following{/other_user}","gists_url":"https://api.github.com/users/gebner/gists{/gist_id}","starred_url":"https://api.github.com/users/gebner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gebner/subscriptions","organizations_url":"https://api.github.com/users/gebner/orgs","repos_url":"https://api.github.com/users/gebner/repos","events_url":"https://api.github.com/users/gebner/events{/privacy}","received_events_url":"https://api.github.com/users/gebner/received_events","type":"User","site_admin":false},"created_at":"2015-09-18T08:26:47Z","updated_at":"2015-09-18T08:26:47Z","body":"So, now `extractInstances` returns a set.  But there are still duplicate edges in the expansion tree."}}