{"entities":{"Q5326318":{"pageid":7355892,"ns":120,"title":"Item:Q5326318","lastrevid":51790415,"modified":"2026-01-20T01:30:14Z","type":"item","id":"Q5326318","labels":{"en":{"language":"en","value":"The MathSAT5 SMT solver"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6194828"}},"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":"Q5326318$C20178E6-87E4-4977-935C-67CA8771341D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e5c5cfd41bd64998e52a9ee652ff09abb75be1cb","datavalue":{"value":{"text":"The MathSAT5 SMT Solver","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5326318$97158716-C94D-4B63-94F1-328CC32FF3C7","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0b217adc32751c3560f83446006333ce12717749","datavalue":{"value":"1381.68153","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$7ED75837-7386-4D8F-965D-0AEB56BFB2E8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d78d3893424bb235c75f3072f93fe1880247ce4a","datavalue":{"value":"10.1007/978-3-642-36742-7_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$60240AB5-24BE-4720-B41B-92F094076C91","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"387e6ac60ed3a0144bb303179c23c53493d401d0","datavalue":{"value":{"entity-type":"item","numeric-id":329418,"id":"Q329418"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$49B74D9F-579E-440B-9C43-201ADC13DCD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e97e7d65eece04188cb1a1dff66ddc09c38fbea4","datavalue":{"value":{"entity-type":"item","numeric-id":479835,"id":"Q479835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$BFB502C0-D978-4CBB-A893-4444A44D6D64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4141b28a9da6f93e8ddbe35f4d6e06c48ff0a627","datavalue":{"value":{"entity-type":"item","numeric-id":5326317,"id":"Q5326317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$042E3752-37BC-4F4B-BFB2-ADEB253DCE51","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4fd5a076641129df5baba24779caed9dec893447","datavalue":{"value":{"entity-type":"item","numeric-id":511776,"id":"Q511776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$CAFBBC2E-DF01-42D4-A881-1C1E37DC0198","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":"Q5326318$CCC187B1-1A1E-45E2-9341-BE4CD9BF0FEE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"95aa5aea465a8772f3ec0450c3b06f16f93c1446","datavalue":{"value":{"time":"+2013-08-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5326318$260B8755-0D6C-4490-98E6-C1FC477480E8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$2D01D7EE-1C71-4B60-B0A5-C1B75E98B91F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$58D15D1E-5F0B-4DB7-830E-2AEE1D5960E4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a1841d694581383c96c3a8ae288e67126b541327","datavalue":{"value":"6194828","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$36728B66-3806-4630-8CEF-016FA8003CBC","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8106193090011d15354793ac9745086e77bdc482","datavalue":{"value":"Q62041183","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$4E6C9935-0994-4EE0-8543-B843A3CED777","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"842bcffb0bb918fd12447e4f670f8dc61d68f929","datavalue":{"value":{"entity-type":"item","numeric-id":21432,"id":"Q21432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$6D61C709-FE73-4614-A333-1454A4BA3B6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e1655b290b91a673f0538ce14f6694f64d961977","datavalue":{"value":{"entity-type":"item","numeric-id":19440,"id":"Q19440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$6DD31071-BF96-4263-92DE-C9BD0C562365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3c6a71142a1c929d2f2ecf037384ebccb9086d6","datavalue":{"value":{"entity-type":"item","numeric-id":21552,"id":"Q21552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$0CE65629-E118-49E4-B4FC-513110425742","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a4f636583a26240d6177ac1ea0a1a2046a522c7b","datavalue":{"value":{"entity-type":"item","numeric-id":21551,"id":"Q21551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$53B16775-3482-42DA-A3F9-1B96A126B073","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"825b8b7cfe525950c0a54b66b3384f77fa2ac0b3","datavalue":{"value":{"entity-type":"item","numeric-id":21553,"id":"Q21553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5326318$F4B1D30F-C640-411B-8ECB-1841D75C845B","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":"Q5326318$F7E79092-4DFA-4871-A406-9B73B1A0D5C1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d96160bef3d1cc9128c1e103ccdfdced4d1ad132","datavalue":{"value":"https://doi.org/10.1007/978-3-642-36742-7_7","type":"string"},"datatype":"url"},"type":"statement","id":"Q5326318$5CE7029E-5944-402F-8AFB-85CDE5EDBFA8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"194f7d795eb2bc7cce9283eaf84f2e7b5696fbe2","datavalue":{"value":"W221832247","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$2FFD722C-8538-44C9-BA83-19E9FAB541C4","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"333d1fe54ada0be996f66bfadca764c890ea200d","datavalue":{"value":"conf/tacas/CimattiGSS13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5326318$98EFC624-F3A1-457A-B662-5C2D4E1CA04D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67ee1543602a49b70abf79c4f9e2688587d1cc15","datavalue":{"value":{"entity-type":"item","numeric-id":862395,"id":"Q862395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4a8a8378bd1392d6ec7b046bd8fd0f6b920de36b","datavalue":{"value":{"amount":"+0.83624666929245","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":"Q5326318$4FEA8683-D315-4275-A931-D48E3AEB9F63","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":"41d3257ed95e9299c5baefadc67e1a3ce685013f","datavalue":{"value":{"amount":"+0.7786802649497986","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":"Q5326318$58A3D681-9745-4939-9C8D-1EBF0C6491A4","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":"39c6ae3c5e3cf9b3de6a33933987fc25c2a9b80a","datavalue":{"value":{"amount":"+0.7639707326889038","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":"Q5326318$1C8A15E5-4B00-4D6F-A51B-5ACB5164B0D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c3e71bfb5b68d2283442ce2c6ed865faa5ef3fdb","datavalue":{"value":{"entity-type":"item","numeric-id":5756564,"id":"Q5756564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43cb7d5f2b2a1c497ac4cf4abddf5c01cdc46f07","datavalue":{"value":{"amount":"+0.7622958421707153","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":"Q5326318$34271A6D-3735-46C2-ABD5-12835ED3E366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44a43da73541e40b8d93166832aeb92cd4bee415","datavalue":{"value":{"entity-type":"item","numeric-id":2830018,"id":"Q2830018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0451db19e21691c9a341f1b20d809e5bebf2b830","datavalue":{"value":{"amount":"+0.7590784430503845","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":"Q5326318$406D38CA-9133-4E88-B66F-D18B64F03963","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5326318","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5326318"}}}}}