{"entities":{"Q17116":{"pageid":17172,"ns":120,"title":"Item:Q17116","lastrevid":56215521,"modified":"2026-03-13T05:27:01Z","type":"item","id":"Q17116","labels":{"en":{"language":"en","value":"Prover9"}},"descriptions":{},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"408d5d53a95de80fc1cb0a11b9848c7d6639e794","datavalue":{"value":"4969","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$EF65B1AF-8D72-4006-AD86-5911A1247FD2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$F47E4403-980E-46A4-BDF9-E6E5F2A42CA9","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"f359dd6e0d1c091e1cbf4262a41ed8c88324b512","datavalue":{"value":"http://www.cs.unm.edu/~mccune/prover9/","type":"string"},"datatype":"url"},"type":"statement","id":"Q17116$C77A718F-2D05-4F41-BB2F-567FD2EE35FD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$3AE51E20-6AD1-4BFB-8559-996011622E83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d379e93a1cc3ab3df2a5b8d85c84eb0620f6469c","datavalue":{"value":"06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$A227C1F2-0757-4A2F-B730-E072D14CF55A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d57514d4788d5abbd1056aadd506bc3f1b86263e","datavalue":{"value":"08","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$04D460CF-3368-44F8-B134-728AC0A1862F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c42d8309659ef226cd875765a3c9064bb7558782","datavalue":{"value":"20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$E1286B6D-9880-485B-80B1-4FE073AB4B8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$EFE5B74B-0B82-4FE6-8A63-C4BE3E9B30AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ae9c75c1f07ce06d85b9552d2104619090f82402","datavalue":{"value":"00","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$BACFF12D-74F5-47BC-AA1D-A92B46E5B7C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ccc624529bfb589cae1d19db3eb04dd4b43978c3","datavalue":{"value":"01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$2184E30C-E1C1-4B73-A2EA-864AE4B096FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$C9A373E6-5B38-468E-A9BE-D181C52F5B9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd4f0694ac7a00e4fadde328cdb4437f6c066de7","datavalue":{"value":"14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$90C7FC6B-E7AE-4BB0-968C-A45909BCFF02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c6cc7c76b3cafafac08dd013fc5ce16db183bb48","datavalue":{"value":"16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$E507C583-E652-4C2D-8FBE-D4B97DABBCB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6652165beef23109cbf13f7bcea8ff518e7cac51","datavalue":{"value":"17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$398EF02C-27BD-4BCC-BFDE-41E42B7BDD00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f50a93e1fa52c1f7a63c5e1d98864f256220e6f","datavalue":{"value":"18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$CD2F27AD-7999-401B-ABEF-7BBE2BFC9B67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"389057ea232b6d266cab69038163241bd07104b6","datavalue":{"value":"51","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$A6670CD7-2A90-4D31-9774-9D603CDF1FBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"85b50fc0bb13fa24d727c960e97501e2c7bce333","datavalue":{"value":"54","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$F1D141C5-EF65-4088-B5A7-397D10B51231","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e24ee68b43931de13fa3c2edb783c4c41f7c841b","datavalue":{"value":"55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$40C97FAF-D81D-4AC0-90C6-2A2B3E7B5D74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cb0bb3315ea6d324166d2a3b9e8cc481541ca3cc","datavalue":{"value":"57","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$B2137274-CA12-4623-BE2B-04DE46059C49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a438efc028ac8f007fcfec586995516429ecdd8","datavalue":{"value":"91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$D73E15DF-5CB5-456B-BC25-BD882DE89745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q17116$EB15C675-7253-4E8A-9292-0CFDEBD0DD00","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2f058c7f37c83e0df243d1b74e064cb4cdf28a10","datavalue":{"value":{"entity-type":"item","numeric-id":18972,"id":"Q18972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$3B389F58-D8F0-4D8E-82F1-9264EADA7727","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6b46a92ecf181aaf6ba95c111143d4a257b6e3e1","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$0CFC1471-4F28-47D2-B2BC-507B46DBCF33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$CD7C0EBB-AFBF-4535-980C-C202C89FA944","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d6d29b9e294eea1a26ce05a4d8663847cfc55575","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$2A27C61D-6831-4998-888E-EAC443F3D1D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$8E3E4FBE-4463-4287-B0FF-877B0A1C386A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$146ECB56-C122-4CC1-9B0A-F4261B1EFA27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"095872c1e8412c6ab0e3851100ddb22b954f588a","datavalue":{"value":{"entity-type":"item","numeric-id":13081,"id":"Q13081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$320464A5-C979-4EC0-A377-7FB7E7CD5ED7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1da83e82f563b21e91a419cb34e11d3be154209f","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$2A45E736-3A56-40D1-9080-1BAD7FA341ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2ded5a481ece08049848bd1edb3f9afa21f0df2f","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$9B4796F7-C2B7-491E-A9E5-C14B9AFE99DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$7BDFCDC0-5C4D-42A3-ABF5-9358C53CE7DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1c7dda9137a8c097a2c877519ded8ad19344712a","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$BE5A5475-0D1A-486F-A827-5B71DF2C0124","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ddfc2dab9f4484d85e8e917c537ee56253d2c6dd","datavalue":{"value":{"entity-type":"item","numeric-id":21735,"id":"Q21735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$63292FE0-2300-4640-82B9-369574BD8BBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f0874088d59a2cbce379152e0f60bc05817c8d64","datavalue":{"value":{"entity-type":"item","numeric-id":21686,"id":"Q21686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$C0619412-62C7-451F-B84D-9A5FBCAD1ABE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"059503b961bdcb19316208c60d7b44e843224e85","datavalue":{"value":{"entity-type":"item","numeric-id":19745,"id":"Q19745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$B7C90C46-FD55-4503-A7B7-71CEC00AC73C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$82EB2944-7536-465E-B04E-B41500A9097C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$D6A33B52-8F64-4449-837D-8B8AA78EB006","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"3780eee939d0a6e96d45e65c74bed949cc1565b3","datavalue":{"value":{"entity-type":"item","numeric-id":13546,"id":"Q13546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$0DF6B7A9-A146-4D64-BFB1-905B1BB58E90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$FDD31EB4-4A40-4426-A15F-BF54D2E85B23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$4F1045B5-D09C-41FB-995F-7B863537623D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2694f9146fdf18f6fd46e48e80fcb9848219fbfd","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q17116$34EF7C26-348A-46BF-A123-56CF925E3A8D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Prover9","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Prover9"}}}}}