{"action":"closed","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/256","labels_url":"https://api.github.com/repos/newca12/gapt/issues/256/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/256/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/256/events","html_url":"https://github.com/newca12/gapt/issues/256","id":55608281,"number":256,"title":"veriT exporter fails with 'undefined formula α'","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/imported","name":"imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-High","name":"Priority-High","color":"FFFFFF"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-01-27T11:51:07Z","updated_at":"2015-01-27T11:51:14Z","closed_at":"2015-01-27T11:51:14Z","body":"_From [stefan.hetzl](https://code.google.com/u/stefan.hetzl/) on December 09, 2013 14:01:06_\n\nMany examples from the cut-introduction test suite that use the EquationalProver fail with:\r\njava.lang.Exception: Undefined formula: α\r\n\tat at.logic.parsing.veriT.VeriTExporter$.at$logic$parsing$veriT$VeriTExporter$$getSymbols(VeriTExporter.scala:69)\r\n[...]\r\n\r\n\r\nFor concrete examples, do:\r\n\r\n:load ../examples/ProofSequences.scala\r\nimport at.logic.provers.eqProver._\r\ncutIntroExp( LinearExampleProof( 4 ), new EquationalProver() )\r\ncutIntroExp( SquareDiagonalExampleProof( 4 ), new EquationalProver() )\r\ncutIntroExp( SumOfOnesF2ExampleProof( 2 ), new EquationalProver() )\r\n\r\ncutIntroExp( loadProver9LKProof( \"../testing/prover9-TSTP/SET/SET154-6/Prover9---1109a.UNS-Ref.s.out\" ), new EquationalProver() )\r\ncutIntroExp( loadProver9LKProof( \"../testing/prover9-TSTP/SEU/SEU188+2/Prover9---1109a.THM-Ref.s.out\" ), new EquationalProver() )\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=256_"}}