{"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:1713516014.0","currentOid":""},"activityList":{"items":[{"before":"b7b6b735d184a050aac77f70cfcc1bd797522e1d","after":"927d1b2b0d7253f7cc6abbf36385da9c95c71341","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-29T08:56:55.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":"Document and refactor KBO::State a bit; add check for global ordering when  manipulating KBO weight in Term","shortMessageHtmlLink":"Document and refactor KBO::State a bit; add check for global ordering…"}},{"before":"e3f9e871c598eac9ce41605c0349201bce375f7c","after":"b7b6b735d184a050aac77f70cfcc1bd797522e1d","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-29T08:42:36.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":"Document and refactor KBO::State a bit; add check for global ordering when  manipulating KBO weight in Term","shortMessageHtmlLink":"Document and refactor KBO::State a bit; add check for global ordering…"}},{"before":"e7aaa9a639021b5f344a9838ebea045bdd6fbd35","after":"39599c2e0cb87b3f1ed924acb8dfb622db5aa4d8","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-29T07:48:15.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":"Refactor preprocessed comparison into separate classes for both LPO and KBO","shortMessageHtmlLink":"Refactor preprocessed comparison into separate classes for both LPO a…"}},{"before":"e046ee1da09d7342b7c03cd5735f0f72e8efca20","after":"e7aaa9a639021b5f344a9838ebea045bdd6fbd35","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-28T16:04:11.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":"Refactor preprocessed comparison into separate classes for both LPO and KBO","shortMessageHtmlLink":"Refactor preprocessed comparison into separate classes for both LPO a…"}},{"before":"c1f622dbb7ffb1441b803c0195f079625effde92","after":"e046ee1da09d7342b7c03cd5735f0f72e8efca20","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-28T15:58:46.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":"Refactor preprocessed comparison into separate classes for both LPO and KBO","shortMessageHtmlLink":"Refactor preprocessed comparison into separate classes for both LPO a…"}},{"before":"933a85007537a636e5912b6e6479fdde7df06d14","after":"c1f622dbb7ffb1441b803c0195f079625effde92","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-28T10:27:14.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 duplicate instructions","shortMessageHtmlLink":"Remove duplicate instructions"}},{"before":"b59cf5fbb2a64f12cdd10fe434e4d62b828e893a","after":"933a85007537a636e5912b6e6479fdde7df06d14","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-27T07:54:33.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":"Do some cleanup","shortMessageHtmlLink":"Do some cleanup"}},{"before":"4c54fa4498777ca7c21a9efa3c02d25db7fad5de","after":"b59cf5fbb2a64f12cdd10fe434e4d62b828e893a","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-27T06:59:49.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":"Rewrite LPO preprocessing yet again, with just one instruction and optimised branching","shortMessageHtmlLink":"Rewrite LPO preprocessing yet again, with just one instruction and op…"}},{"before":"6e3e03d1f35b95a2be4c04892530fc016c14891c","after":"21e4ffce284d01bed370c0c8affb45c310b8961b","ref":"refs/heads/upcop","pushedAt":"2024-04-26T15:45:41.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":"randomise models","shortMessageHtmlLink":"randomise models"}},{"before":"57debfd68c9fabe90f96810f21ff4703e6eba611","after":"4c54fa4498777ca7c21a9efa3c02d25db7fad5de","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-26T09:58:49.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":"Use absolute positions in jumps","shortMessageHtmlLink":"Use absolute positions in jumps"}},{"before":"ca653daea10eaba4b797b857a62c9de9b5e72b11","after":"e3f9e871c598eac9ce41605c0349201bce375f7c","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-26T09:28:09.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":"Put applicators into anonymous namespaces to avoid linker collisions","shortMessageHtmlLink":"Put applicators into anonymous namespaces to avoid linker collisions"}},{"before":"8aeec54124b120ac121266f4f8a5d8196c9f36c7","after":"ca653daea10eaba4b797b857a62c9de9b5e72b11","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-26T08:52:49.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 new functions as not implemented to SKIKBO and make them pure virtual instead","shortMessageHtmlLink":"Move new functions as not implemented to SKIKBO and make them pure vi…"}},{"before":"51ebfade70dfac6b3d8654b12f54ac4a7dc37d0c","after":"8aeec54124b120ac121266f4f8a5d8196c9f36c7","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-26T08:39:24.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":"Review: fw demodulation applicator, appliedterm documentation and refactor","shortMessageHtmlLink":"Review: fw demodulation applicator, appliedterm documentation and ref…"}},{"before":"bbfe687fe776cd5d9755b56f86d2976279a32985","after":"51ebfade70dfac6b3d8654b12f54ac4a7dc37d0c","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-26T07:31:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"joe-hauns","name":"Joe Hauns","path":"/joe-hauns","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/28921820?s=80&v=4"},"commit":{"message":"cosmetics","shortMessageHtmlLink":"cosmetics"}},{"before":"81301ee7e29c1b990cef912df57db090a7611370","after":"6e3e03d1f35b95a2be4c04892530fc016c14891c","ref":"refs/heads/upcop","pushedAt":"2024-04-25T13:18:12.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":"whatever this is, it's much faster","shortMessageHtmlLink":"whatever this is, it's much faster"}},{"before":"9b2d3cf86334f05d55ad16726a6f48cb0fd79eeb","after":"57debfd68c9fabe90f96810f21ff4703e6eba611","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-25T13:07:26.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":"Add initial linearized version","shortMessageHtmlLink":"Add initial linearized version"}},{"before":"5d3e67fba5fb48a790f473a311e718a1e0237970","after":"81301ee7e29c1b990cef912df57db090a7611370","ref":"refs/heads/upcop","pushedAt":"2024-04-25T11:45:20.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"MichaelRawson","name":"Michael Rawson","path":"/MichaelRawson","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1696762?s=80&v=4"},"commit":{"message":"back to something halfway sane","shortMessageHtmlLink":"back to something halfway sane"}},{"before":"638444972e0dbdd6ce4188cd839353acd0d4488f","after":"9b2d3cf86334f05d55ad16726a6f48cb0fd79eeb","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-24T14:44:36.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 it simpler by using a conditional operator","shortMessageHtmlLink":"Make it simpler by using a conditional operator"}},{"before":"e732f12bda4a502a2b2ff390d7326738f183cead","after":"3cefe51846c5fc20b05e4676068f416972c107e9","ref":"refs/heads/robin_c-sat-s-sr-for-master","pushedAt":"2024-04-24T12:34:43.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":"implement revisions suggested by Michael","shortMessageHtmlLink":"implement revisions suggested by Michael"}},{"before":"c51c744dfb9470fe0663833b8163b0e3b8237df1","after":"638444972e0dbdd6ce4188cd839353acd0d4488f","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-24T09:36:12.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":"Some small improvements","shortMessageHtmlLink":"Some small improvements"}},{"before":"49251c401bff5d00d209e22162406a99b060a52d","after":"c51c744dfb9470fe0663833b8163b0e3b8237df1","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-24T08:49:16.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":"Some relatively stable intermediate state","shortMessageHtmlLink":"Some relatively stable intermediate state"}},{"before":"79fd6d09c61912d456eeb27ae4f3ca2d566616d0","after":"bbfe687fe776cd5d9755b56f86d2976279a32985","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-24T07:21:55.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":"Review","shortMessageHtmlLink":"Review"}},{"before":"b49fa41923eb1e726eb8cf3e6a738b6e6defed54","after":"49251c401bff5d00d209e22162406a99b060a52d","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-23T13:44:13.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":"Merge branch 'ordering-applied-term-isgreater' into demodulation-improvements","shortMessageHtmlLink":"Merge branch 'ordering-applied-term-isgreater' into demodulation-impr…"}},{"before":"654c52ae41cea7f9e6849c3a7c26ebc62471757c","after":"b49fa41923eb1e726eb8cf3e6a738b6e6defed54","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-23T13:39:14.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"mezpusz","name":"Márton Hajdu","path":"/mezpusz","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5413430?s=80&v=4"},"commit":{"message":"Merge branch 'ordering-applied-term-isgreater' into demodulation-improvements","shortMessageHtmlLink":"Merge branch 'ordering-applied-term-isgreater' into demodulation-impr…"}},{"before":"35dd7f4f6b0bd32e5dfed257cc13259406aebc6b","after":"79fd6d09c61912d456eeb27ae4f3ca2d566616d0","ref":"refs/heads/ordering-applied-term-isgreater","pushedAt":"2024-04-23T12:18:06.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":"Review","shortMessageHtmlLink":"Review"}},{"before":"d9be6536c4caea3ac23017dfd653444c94d24ebb","after":"654c52ae41cea7f9e6849c3a7c26ebc62471757c","ref":"refs/heads/demodulation-improvements","pushedAt":"2024-04-23T11:29:15.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":"Add a simpler and (mostly correct) yet still inefficient version","shortMessageHtmlLink":"Add a simpler and (mostly correct) yet still inefficient version"}},{"before":"828ae2e8777288d6b950b1b91795b85c07737883","after":"b0fb7be1ea630e61685addfbc7c4ff96bdd4957f","ref":"refs/heads/martin-streamline-qa","pushedAt":"2024-04-23T04:29:30.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":"protect term algebra discriminators from getting flipped","shortMessageHtmlLink":"protect term algebra discriminators from getting flipped"}},{"before":"7e4f17d9e66f1850b78e752920c4eb797cfebf3d","after":"828ae2e8777288d6b950b1b91795b85c07737883","ref":"refs/heads/martin-streamline-qa","pushedAt":"2024-04-22T15:49:35.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 getParents also for the Z3 version","shortMessageHtmlLink":"update getParents also for the Z3 version"}},{"before":"a78119973c96403b8d43a9ec09618f067c3eaba7","after":"7e4f17d9e66f1850b78e752920c4eb797cfebf3d","ref":"refs/heads/martin-streamline-qa","pushedAt":"2024-04-22T15:25:17.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":"derivedFromInput can be established in minimizeAncestorsAndUpdateSelectedStats, thus Giles' checks moved into UIHelper::outputResult, turned into INVALID_OPERATION (admit we are wrong when we are), careful also to update isPureTheoryDescendant during the traversal","shortMessageHtmlLink":"derivedFromInput can be established in minimizeAncestorsAndUpdateSele…"}},{"before":"302e4359820c6f97ef6a3639c0afdcada12ee649","after":"a78119973c96403b8d43a9ec09618f067c3eaba7","ref":"refs/heads/martin-streamline-qa","pushedAt":"2024-04-22T11:10:23.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"quickbeam123","name":"Martin Suda","path":"/quickbeam123","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5189025?s=80&v=4"},"commit":{"message":"fixing a bug in determining the actual inputType after minimization; we now need to be strict and make all AVATAR_DEFINITIONs Axioms (before we were inheriting goaledness from the caulal parent for a better goal-directed search","shortMessageHtmlLink":"fixing a bug in determining the actual inputType after minimization; …"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEPMKXbAA","startCursor":null,"endCursor":null}},"title":"Activity · vprover/vampire"}