{"entities":{"Q5458346":{"pageid":7487905,"ns":120,"title":"Item:Q5458346","lastrevid":96234884,"modified":"2026-06-05T10:45:03Z","type":"item","id":"Q5458346","labels":{"en":{"language":"en","value":"Rocket-Fast Proof Checking for SMT Solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5262393"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$639C19ED-8043-46BD-9077-8A12A4A805AE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ff500f030d8b1ddea58d6ac916b37595934d33a7","datavalue":{"value":{"text":"Rocket-Fast Proof Checking for SMT Solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5458346$2DF24BAC-3790-4D2E-B8DA-3E09A7211BD8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"335a92d4cdaf3dbb97f8364098d6ef1a8ba4914c","datavalue":{"value":"1134.68492","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458346$94E1533A-9DF0-4F3F-8BB2-FB773C319395","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"88125e7b958726276118bf30ae157b285114c374","datavalue":{"value":"10.1007/978-3-540-78800-3_38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458346$2B0840B1-6134-4547-8EDD-E2D54E5C14AF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e8b58aa56bc8beed0a4159e66079e561cc626cb9","datavalue":{"value":{"entity-type":"item","numeric-id":2655334,"id":"Q2655334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$EBE038F3-C0DF-4579-9CF4-150A712D73BA","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0caef843b05c7cfb5667c1a8106613cbf61a6d23","datavalue":{"value":{"entity-type":"item","numeric-id":2894263,"id":"Q2894263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$CB911C14-DF85-450C-A5AB-C2E7E7133459","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de5306c1211a7dcd78b6214088eb3e5b7092fd16","datavalue":{"value":{"time":"+2008-04-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5458346$3B8FB0EF-700E-4F9F-B78D-C676DBC357DA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458346$65D11849-479B-4936-AC76-F717E0BC736A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7f0088bf0c1da865472cdf27e22184f4c21f7312","datavalue":{"value":"5262393","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458346$3439798D-D837-4BA4-B71D-5F0993F300FB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$A6429C41-576C-4FE2-B1D0-72DB634942F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"cd543fd49199b1838ba332ea5e7b335fbe6c5a58","datavalue":{"value":{"entity-type":"item","numeric-id":19608,"id":"Q19608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$E8ACBBB2-751A-4F1F-AB96-A884082CE698","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$BAA3E8A6-2292-4AAC-8DCC-0451C34560E4","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$8C3497A2-0A88-4D6C-860D-28BCBE9A9D57","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c65692056cb7ac7edaa034df115283c23d56e2eb","datavalue":{"value":"https://doi.org/10.1007/978-3-540-78800-3_38","type":"string"},"datatype":"url"},"type":"statement","id":"Q5458346$01EE1B0A-061A-45E5-A002-C76F52DF72C1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1bb263e66ef560ecf585888f6d2485eae4fe9f58","datavalue":{"value":"W155339612","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458346$2A444519-FAF2-4A9C-A7EF-CDD43CA2C6E4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9be67f799ffc5b3fd133657f657d0609a463820d","datavalue":{"value":{"entity-type":"item","numeric-id":5312942,"id":"Q5312942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$B2B3C316-E4AE-4E4F-B5F9-6CC42F357947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ef99484234e0e2307a8d429f1e1a558442d61af","datavalue":{"value":{"entity-type":"item","numeric-id":2703706,"id":"Q2703706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$9E2702DD-E767-4BBD-B4ED-332F5797EA65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dda516360752f06de61020226a14fa7cfc2fbf83","datavalue":{"value":{"entity-type":"item","numeric-id":2864404,"id":"Q2864404"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$09FA2F26-BDA4-40AF-A5AA-7E6E26FC382E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$9F735C9B-CB3B-4081-BA65-51868ABBD2B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b4f714dbb33bba32b50777c1d77c1cb7ff5fe56","datavalue":{"value":{"entity-type":"item","numeric-id":3608773,"id":"Q3608773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$1C0AE451-7AA7-4D7C-A767-8285CB739201","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04c0523630e1e6c8f44c947a834580b7eb080727","datavalue":{"value":{"entity-type":"item","numeric-id":2486578,"id":"Q2486578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$3406FF98-5411-405D-845D-8E68F22595B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$94DBAA05-09E6-4A75-8ACA-F3DBA855BB08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e6b26606a781175a19b1c8fcba43abdeea964791","datavalue":{"value":{"entity-type":"item","numeric-id":2848688,"id":"Q2848688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$D833C924-CC07-4D02-ACBC-2A9939E0938F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"30da8148c90aaf17fe8a996c8559dd1f27b45ebd","datavalue":{"value":{"entity-type":"item","numeric-id":4809074,"id":"Q4809074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458346$C7311D09-2194-42CC-BBDB-94C381777CDD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dc4a898c2ce53e9d3b4432ba9d09cae8e716f24","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e87c2b24fba1ae700305731b7358a85142d9b41f","datavalue":{"value":{"amount":"+0.8209550380706787","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5458346$8D34121E-49E0-45C7-AAC3-B5D1E3D951CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82887add6ef83bf1d5f825462c68445edf602b89","datavalue":{"value":{"amount":"+0.8107829093933105","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5458346$D82BC938-E6D6-4CBC-8FAB-A514CC2F92F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"18ba98873d052f5816175646d512a17079b79c03","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c3544525f252d784487dfed9f8b247765b450132","datavalue":{"value":{"amount":"+0.7887179851531982","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5458346$02CB7A64-6CD4-4E33-B2BB-5D8AEF5D80C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d13a1aa7335cec291b0dfd74d25004b6bcf26c1d","datavalue":{"value":{"entity-type":"item","numeric-id":3460065,"id":"Q3460065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"989f8cf81eae35ae540dc828644fcd3f8679dcf1","datavalue":{"value":{"amount":"+0.7872762680053711","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5458346$50FE3DAF-6751-43A1-B003-27CEE23899DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1f943c54080b27de44312af7634875e7f707904","datavalue":{"value":{"entity-type":"item","numeric-id":5716582,"id":"Q5716582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eef1f6b6f14886c5baea6b7bbdb3a12943d073ba","datavalue":{"value":{"amount":"+0.785442590713501","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5458346$D32E5B2C-0DE0-44BB-B726-082C6A73CC57","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Rocket-Fast Proof Checking for SMT Solvers","badges":[]}}}}}