{"entities":{"Q21698":{"pageid":21754,"ns":120,"title":"Item:Q21698","lastrevid":56241696,"modified":"2026-03-13T05:42:26Z","type":"item","id":"Q21698","labels":{"en":{"language":"en","value":"CBMC"}},"descriptions":{},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"3b0ca11b166f5ec9f2d95f576c6ab0bf48335199","datavalue":{"value":"9719","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$439503A2-C4C3-4CE1-97F1-44F2CA1692A2","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":"Q21698$A11D1465-21FE-4E33-94EB-4C3BA660B7DD","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"b9590887b2cf46df06248b8ef9bca6e00361cb48","datavalue":{"value":"http://www.cprover.org/cbmc/","type":"string"},"datatype":"url"},"type":"statement","id":"Q21698$66B73CAB-DCB0-496E-999E-CDC685E103D4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$26AD4194-5C09-4982-BF39-7CFE26882357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$9C572161-B367-4F60-94C0-65114C67684A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$E0626F49-23B9-418A-9CDD-D535D939B7F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7bfd76a3cee4b1dd54b082650152581ca2d695de","datavalue":{"value":"93","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$F165A362-E965-455F-8FBF-DD2E6EDA934A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$628BC574-B55E-43D7-8913-1247D65AAF3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ae9c75c1f07ce06d85b9552d2104619090f82402","datavalue":{"value":"00","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$CD393371-A957-4FE2-A477-FD2A1644AD2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$2E9B95C2-65BA-49BB-9E79-6E9C8D0B6407","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a104733b1e30d91f56342777dc887a3edbb9e05f","datavalue":{"value":"65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$DE732432-271A-452D-BDC7-A220D0D034FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"eafc2970861edb4c7004312b82ba31ab41f8cd06","datavalue":{"value":"76","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$02B1D232-CA65-4A7B-9871-9658B43BD8DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4edc7e695c3667a3dc24594c0516548b87f81467","datavalue":{"value":"81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$4B7336DD-B475-409F-BAE3-9D1297D9D31D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a438efc028ac8f007fcfec586995516429ecdd8","datavalue":{"value":"91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$950248B0-A31D-420A-B1D5-175302C4E69B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d0cfa49f62a5e301328cd7af9d04a50119944fd5","datavalue":{"value":"92","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q21698$BECADF90-F30D-4BC4-946D-BDC2CF28F2E7","rank":"normal"}],"P1458":[{"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":"Q21698$E737E401-C577-4472-8D04-868EE796207E","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":"Q21698$08A20CAD-48D2-45E4-A930-F98F1BB4E1A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"506ca92f4d2e993af30c0ddbc6e82ee43fd41020","datavalue":{"value":{"entity-type":"item","numeric-id":15473,"id":"Q15473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$A4360FE6-E18E-4FCD-BAB3-3A0860A52CAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0566ad334499237f2689386a24c3ff4452487d83","datavalue":{"value":{"entity-type":"item","numeric-id":15987,"id":"Q15987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$82406727-D654-43B0-A32D-353A2F11E1A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$AB60AEF1-0395-47C8-B972-23D54BE4CC2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4bd7f70eb24c576b3e3d45c70855bbd63c624f67","datavalue":{"value":{"entity-type":"item","numeric-id":19440,"id":"Q19440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$1E564C3D-8ED2-42C6-BC4F-83FC8AA15DEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9b69dfd6aefb61fb62fe0c9bd5bda4c391dd9a94","datavalue":{"value":{"entity-type":"item","numeric-id":17045,"id":"Q17045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$22A62D25-A0EF-4293-8050-C9177447406E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"6cce9708c735eca903b9027de804184e2f0ded4b","datavalue":{"value":{"entity-type":"item","numeric-id":15668,"id":"Q15668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$3DF8D877-7866-4D5A-B53E-430DBA2F4DAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c727518dabc166c675c7b43ae93b867ba73107c6","datavalue":{"value":{"entity-type":"item","numeric-id":19309,"id":"Q19309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$5FB52EFD-6715-433E-A043-707D75EE96F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"1c43eb26b29c59c3376a4b82a5c62f435fb00011","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$2980B741-6B74-4733-B1DC-3E947E42167B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"15cf6162efa291cebe5dd972dfa4eff00017a3e7","datavalue":{"value":{"entity-type":"item","numeric-id":12944,"id":"Q12944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$FC205444-CD1C-41E3-BBF0-8425DC2F721F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7328564303d1929bbeab82ebc64c91f01ea9372b","datavalue":{"value":{"entity-type":"item","numeric-id":19680,"id":"Q19680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$FDF994A3-276A-4165-B037-88E4AB736845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cd85ea4235f75e500e615783d8111edd91d3a41d","datavalue":{"value":{"entity-type":"item","numeric-id":16316,"id":"Q16316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$9EC21938-ECAD-4749-B36B-EDA4EC56486E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8aafdf7df9ab6945d55471b6dee241d20aae57bb","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$FF88663D-1C76-44FA-B2E3-6593226672E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"296077a8a33e3821efa88523c9bdcc7d2eedc6e1","datavalue":{"value":{"entity-type":"item","numeric-id":38420,"id":"Q38420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$62974859-F5A6-4BE7-B529-F16550E96A6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2e072a738543502cb1df91e8cb89fd6f06eabadf","datavalue":{"value":{"entity-type":"item","numeric-id":17043,"id":"Q17043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$6FDD7615-2CC6-422E-A744-5A5FD124B264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"346bb06feebe5eec8261e483309d0da7485c1091","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$06FB9599-201C-4E88-8E85-14E0EE9A8F64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"187424f3f1f0faaf242dd7691ed1bbf9d5e5d9ae","datavalue":{"value":{"entity-type":"item","numeric-id":25618,"id":"Q25618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$8A351DFD-9BB4-4064-BC75-25890883A57C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"fbf202ee2b6e5912a6faa7a88e6e3186417d8860","datavalue":{"value":{"entity-type":"item","numeric-id":24728,"id":"Q24728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$D36FC2AF-2783-4F64-92ED-5D3A9CBFDB41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0c862528104c319162f0714346b07f5cce70fb7c","datavalue":{"value":{"entity-type":"item","numeric-id":35084,"id":"Q35084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q21698$0612BB24-4333-4FE5-9B48-691131E6D2B3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CBMC","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CBMC"}}}}}