{"action":"opened","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/265","labels_url":"https://api.github.com/repos/newca12/gapt/issues/265/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/265/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/265/events","html_url":"https://github.com/newca12/gapt/issues/265","id":55608501,"number":265,"title":"Expansion Tree extraction fails in new lambda branch:","user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/newca12/gapt/labels/1%20star","name":"1 star","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/bug","name":"bug","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Component-ProofTransformations","name":"Component-ProofTransformations","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/imported","name":"imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Milestone-Release7.0","name":"Milestone-Release7.0","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-Medium","name":"Priority-Medium","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-01-27T11:53:15Z","updated_at":"2015-01-27T11:53:15Z","closed_at":null,"body":"_From [Martin.R...@googlemail.com](https://code.google.com/u/113922991942493634983/) on May 07, 2014 13:55:43_\n\nOn the cli call:\r\n\r\n    val pdb = loadLLK(\"algorithms/llk/src/test/resources/pigeon32.llk\")\r\n    extractExpansionTrees(pdb.proof(\"PROOF\"))\r\n\r\nresults in:\r\njava.lang.IllegalArgumentException: Bug in merge in extractExpansionTrees. By Construction, the trees to be merge should have the same structure, which is violated for:\r\nAtom(=:(ι->(ι->ο))(hole:(ι->ι)(pigeon1:ι):ι, 0:ι): o)∧Atom(=:(ι->(ι->ο))(hole:(ι->ι)(pigeon2:ι):ι, 0:ι): o)\r\nAtom((=:(ι->(ι->ο))(hole:(ι->ι)(pigeon1:ι):ι, 0:ι): o∧=:(ι->(ι->ο))(hole:(ι->ι)(pigeon2:ι):ι, 0:ι): o))\r\n\tat at.logic.calculi.expansionTrees.merge$.doApplyMerge(expansionTrees.scala:693)\r\n\tat at.logic.calculi.expansionTrees.merge$.start_op2$2(expansionTrees.scala:643)\r\n\tat at.logic.calculi.expansionTrees.merge$.doApplyMerge(expansionTrees.scala:677)\r\n\tat at.logic.calculi.expansionTrees.merge$.at$logic$calculi$expansionTrees$merge$$detectAndMergeMergeNodes(expansionTrees.scala:625)\r\n\tat at.logic.calculi.expansionTrees.merge$$anonfun$at$logic$calculi$expansionTrees$merge$$detectAndMergeMergeNodes$1.apply(expansionTrees.scala:605)\r\n\tat at.logic.calculi.expansionTrees.merge$$anonfun$at$logic$calculi$expansionTrees$merge$$detectAndMergeMergeNodes$1.apply(expansionTrees.scala:603)\r\n\tat scala.collection.immutable.List.foreach(List.scala:318)\r\n\tat at.logic.calculi.expansionTrees.merge$.at$logic$calculi$expansionTrees$merge$$detectAndMergeMergeNodes(expansionTrees.scala:603)\r\n\tat at.logic.calculi.expansionTrees.merge$.doApplyMerge(expansionTrees.scala:670)\r\n\tat at.logic.calculi.expansionTrees.merge$.doApplyMerge(expansionTrees.scala:680)\r\n\tat at.logic.calculi.expansionTrees.merge$.at$logic$calculi$expansionTrees$merge$$detectAndMergeMergeNodes(expansionTrees.scala:625)\r\n\tat at.logic.calculi.expansionTrees.merge$.main(expansionTrees.scala:557)\r\n\tat at.logic.calculi.expansionTrees.merge$.applyRec$1(expansionTrees.scala:526)\r\n\tat at.logic.calculi.expansionTrees.merge$.apply(expansionTrees.scala:538)\r\n\tat at.logic.transformations.herbrandExtraction.extractExpansionTrees$.apply(expansionTrees.scala:13)\r\n\r\nThe proof in question is first-order with equations in it, but does not do equational inference. Do you know what the reason for the failure is?\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=265_"}}