{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":18067910,"defaultBranch":"master","name":"vampire","ownerLogin":"vprover","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2014-03-24T15:46:00.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/6704909?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1727115285.0","currentOid":""},"activityList":{"items":[{"before":"bac46e7bdc6f4178c624f5ff52e41924586694ff","after":"6322f649d3a4dc7f2de905ca645afa547e69a9c0","ref":"refs/heads/michael-undeclared-typecon","pushedAt":"2024-09-23T19:55:19.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"raise USER_ERROR on undeclared type constructor","shortMessageHtmlLink":"raise USER_ERROR on undeclared type constructor"}},{"before":"85ba823be093ef1fb057b457f2c23757a969327a","after":"75742d60e723da6da1c7ecff9a3b38bc02dd4fa3","ref":"refs/heads/master","pushedAt":"2024-09-23T19:54:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"no longer need to find our own Vampire","shortMessageHtmlLink":"no longer need to find our own Vampire"}},{"before":null,"after":"bac46e7bdc6f4178c624f5ff52e41924586694ff","ref":"refs/heads/michael-undeclared-typecon","pushedAt":"2024-09-23T18:14:45.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"raise USER_ERROR on undeclared type constructor","shortMessageHtmlLink":"raise USER_ERROR on undeclared type constructor"}},{"before":"127d37970d8e6a4f961eb32875f8bc0b6512d05a","after":"85ba823be093ef1fb057b457f2c23757a969327a","ref":"refs/heads/master","pushedAt":"2024-09-23T17:35:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"simplify binary naming for CMake build","shortMessageHtmlLink":"simplify binary naming for CMake build"}},{"before":"a40cd71ae767f5c14b8daf43368bdbbe041896d6","after":"6aa049ef259483fa016da3e863be97bcd5ff040d","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-23T17:32:11.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge branch 'master' into conditional-redundancy","shortMessageHtmlLink":"Merge branch 'master' into conditional-redundancy"}},{"before":"0e8176799ed2eecdb56b7eb38561ff95773702eb","after":"127d37970d8e6a4f961eb32875f8bc0b6512d05a","ref":"refs/heads/master","pushedAt":"2024-09-23T14:58:03.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"Merge pull request #610 from kazarmy/REV_COUNT=OFF\n\nAdd `-DREV_COUNT=OFF` build option","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2542765844\" data-permission-text=\"Title is private\" data-url=\"https://github.com/vprover/vampire/issues/610\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/vprover/vampire/pull/610/hovercard\" href=\"https://github.com/vprover/vampire/pull/610\">#610</a> from kazarmy/REV_COUNT=OFF"}},{"before":"619127915612af00c7d8724f2351c1e8444548ab","after":"305297131e88153c50d495e69d311fd75b602e4e","ref":"refs/heads/michael-proof-extra","pushedAt":"2024-09-23T10:04:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"keep the free class of proof_extra","shortMessageHtmlLink":"keep the free class of proof_extra"}},{"before":"34c92d76df7f4de91b5ec579e95f33c63da61da1","after":"a40cd71ae767f5c14b8daf43368bdbbe041896d6","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-23T09:59:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Remove unification from LPOComparator; improve and factor out cache usage","shortMessageHtmlLink":"Remove unification from LPOComparator; improve and factor out cache u…"}},{"before":"6d044da09cbf54928e7ad628b561a200971128f1","after":"34c92d76df7f4de91b5ec579e95f33c63da61da1","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-23T09:11:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Move check to OrderingComparator; expand is now the only virtual method of OrderingComparator","shortMessageHtmlLink":"Move check to OrderingComparator; expand is now the only virtual meth…"}},{"before":"1684599355c85effe118d14d6035adc31c8d64fc","after":"6d044da09cbf54928e7ad628b561a200971128f1","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-21T19:47:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Fix KBOComparator expansion","shortMessageHtmlLink":"Fix KBOComparator expansion"}},{"before":"c7f16475d5dbbcb9fe89df6a12cabfeb57582a1c","after":"1684599355c85effe118d14d6035adc31c8d64fc","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-21T18:08:18.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Unify the OrderingComparator implementations to some degree","shortMessageHtmlLink":"Unify the OrderingComparator implementations to some degree"}},{"before":"624bbb7f29c942a5fa005d8929a91e300ecf7b67","after":"c7f16475d5dbbcb9fe89df6a12cabfeb57582a1c","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-21T10:51:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Try unifying matcher and removingmatcher","shortMessageHtmlLink":"Try unifying matcher and removingmatcher"}},{"before":"500917647d1f324ed9665dee838da65a9773490a","after":"624bbb7f29c942a5fa005d8929a91e300ecf7b67","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-21T10:45:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Try unifying matcher and removingmatcher","shortMessageHtmlLink":"Try unifying matcher and removingmatcher"}},{"before":"77741b29ce97ac0a4da02f5be72e5540d0ae5440","after":"ca36015adf4575796dba69038951d5b87bd2b328","ref":"refs/heads/optimise-instance-redundancy-handler","pushedAt":"2024-09-21T09:46:10.000Z","pushType":"push","commitsCount":15,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge branch 'master' into optimise-instance-redundancy-handler","shortMessageHtmlLink":"Merge branch 'master' into optimise-instance-redundancy-handler"}},{"before":"4db5f6bc80cad44b1d9347db5bbdc9b35fd0f567","after":"500917647d1f324ed9665dee838da65a9773490a","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-21T08:46:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Implement merging ordering comparators -- needs lot of work, but not completely inefficient","shortMessageHtmlLink":"Implement merging ordering comparators -- needs lot of work, but not …"}},{"before":"2c513e92d147399b54c8c10a55920e0e1f73286e","after":"72e486cce1b0d301959c053d98d0c222d7207d06","ref":"refs/heads/sat-subsumption-debug-check-for-code-trees","pushedAt":"2024-09-20T12:25:02.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Add debug checks to code tree subsumption; clean up code","shortMessageHtmlLink":"Add debug checks to code tree subsumption; clean up code"}},{"before":null,"after":"2c513e92d147399b54c8c10a55920e0e1f73286e","ref":"refs/heads/sat-subsumption-debug-check-for-code-trees","pushedAt":"2024-09-20T12:21:37.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Add debug checks to code tree subsumption; clean up code","shortMessageHtmlLink":"Add debug checks to code tree subsumption; clean up code"}},{"before":null,"after":"619127915612af00c7d8724f2351c1e8444548ab","ref":"refs/heads/michael-proof-extra","pushedAt":"2024-09-20T12:16:47.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"add resolution, demodulation, equality resolution","shortMessageHtmlLink":"add resolution, demodulation, equality resolution"}},{"before":"f9d43887d23967627e00eca5cef89ca4fb2a5a00","after":"17e73dc7218823134b08a89509db6b2fee974064","ref":"refs/heads/robin-all-subsumption-resolutions","pushedAt":"2024-09-20T11:58:20.000Z","pushType":"push","commitsCount":13,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge branch 'master' into robin-all-subsumption-resolutions","shortMessageHtmlLink":"Merge branch 'master' into robin-all-subsumption-resolutions"}},{"before":"8c28f60f5abd5e7bed99bcb6c9b4ca17628539e3","after":"f9d43887d23967627e00eca5cef89ca4fb2a5a00","ref":"refs/heads/robin-all-subsumption-resolutions","pushedAt":"2024-09-20T11:12:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"RobCoutel","name":"Robin Coutelier","path":"/RobCoutel","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/57060640?s=80&v=4"},"commit":{"message":"refactored the function to check if SR is possible with specific literal","shortMessageHtmlLink":"refactored the function to check if SR is possible with specific literal"}},{"before":"f199c0acdf22c33b45715211985a73b409a99f9f","after":"0e8176799ed2eecdb56b7eb38561ff95773702eb","ref":"refs/heads/master","pushedAt":"2024-09-20T08:39:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"quickbeam123","name":"Martin Suda","path":"/quickbeam123","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5189025?s=80&v=4"},"commit":{"message":"update the samplers to support cts","shortMessageHtmlLink":"update the samplers to support cts"}},{"before":"9641e6a00bda234257e7230edfde86611ce4250c","after":"f32aa85d0c75b21fdb1ed2056c064a02e83727e4","ref":"refs/heads/mtpa","pushedAt":"2024-09-20T07:38:48.000Z","pushType":"push","commitsCount":14,"pusher":{"login":"quickbeam123","name":"Martin Suda","path":"/quickbeam123","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5189025?s=80&v=4"},"commit":{"message":"Merge branch 'master' into mtpa","shortMessageHtmlLink":"Merge branch 'master' into mtpa"}},{"before":"38429ed57cff73fa924a845b4aa89a90d4fd198a","after":"f199c0acdf22c33b45715211985a73b409a99f9f","ref":"refs/heads/master","pushedAt":"2024-09-20T07:38:29.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"quickbeam123","name":"Martin Suda","path":"/quickbeam123","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5189025?s=80&v=4"},"commit":{"message":"cts on by default","shortMessageHtmlLink":"cts on by default"}},{"before":"84732ea92d41fa8adac81ef619872d10d62df5b7","after":"23c55a0b24fea65c9ed2165e7ff3fbce97545fce","ref":"refs/heads/simplify-flatterm","pushedAt":"2024-09-20T07:25:02.000Z","pushType":"push","commitsCount":12,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge branch 'master' into simplify-flatterm","shortMessageHtmlLink":"Merge branch 'master' into simplify-flatterm"}},{"before":"df8a2cf317c2a6e63ad42b9ab036df98dc418047","after":"4db5f6bc80cad44b1d9347db5bbdc9b35fd0f567","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-20T07:07:28.000Z","pushType":"push","commitsCount":11,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge branch 'master' into conditional-redundancy","shortMessageHtmlLink":"Merge branch 'master' into conditional-redundancy"}},{"before":"6df44618720d166b4dd6ecfacf279bf4437ffe9b","after":null,"ref":"refs/heads/code-tree-subsumption","pushedAt":"2024-09-19T20:07:28.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"}},{"before":"f0a7bc979451496f1a7bb30614f0c1239712ff62","after":"38429ed57cff73fa924a845b4aa89a90d4fd198a","ref":"refs/heads/master","pushedAt":"2024-09-19T20:07:23.000Z","pushType":"pr_merge","commitsCount":8,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"Merge pull request #605 from vprover/code-tree-subsumption\n\nCode tree subsumption","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2533013394\" data-permission-text=\"Title is private\" data-url=\"https://github.com/vprover/vampire/issues/605\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/vprover/vampire/pull/605/hovercard\" href=\"https://github.com/vprover/vampire/pull/605\">#605</a> from vprover/code-tree-subsumption"}},{"before":"4288d86b61ab4c0d837740e63aa68595625dd317","after":"6df44618720d166b4dd6ecfacf279bf4437ffe9b","ref":"refs/heads/code-tree-subsumption","pushedAt":"2024-09-19T18:40:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Make bithacking in CodeTree::CodeOp more robust","shortMessageHtmlLink":"Make bithacking in CodeTree::CodeOp more robust"}},{"before":null,"after":"df8a2cf317c2a6e63ad42b9ab036df98dc418047","ref":"refs/heads/conditional-redundancy","pushedAt":"2024-09-19T18:36:20.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge some entries in ConstraintIndex; add reversed ordering constraint to result of superpositions; modify KBOComparator to a similar structure as LPOComparator","shortMessageHtmlLink":"Merge some entries in ConstraintIndex; add reversed ordering constrai…"}},{"before":"dd9b7a2c6b944cfe56266c5c3fcea7ca0eb985ef","after":"9b10ff2287d223f09bf300f58095373d19ca3390","ref":"refs/heads/michael-slowmotion","pushedAt":"2024-09-18T17:25:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"remember to rename clauses apart","shortMessageHtmlLink":"remember to rename clauses apart"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yM1QxOTo1NToxOS4wMDAwMDBazwAAAAS-Yo8P","startCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0yM1QxOTo1NToxOS4wMDAwMDBazwAAAAS-Yo8P","endCursor":"Y3Vyc29yOnYyOpK7MjAyNC0wOS0xOFQxNzoyNTo1MC4wMDAwMDBazwAAAAS5-9zV"}},"title":"Activity · vprover/vampire"}