{"entities":{"Q6039408":{"pageid":13121154,"ns":120,"title":"Item:Q6039408","lastrevid":47847658,"modified":"2026-01-02T21:02:55Z","type":"item","id":"Q6039408","labels":{"en":{"language":"en","value":"The proof complexity of SMT solvers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7682383"}},"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":"Q6039408$E30A75CB-ADBF-4B8B-BB1E-13A0B3CA741A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9fd6223bd2b1d80a05aff0f5785999e2ee008247","datavalue":{"value":{"text":"The proof complexity of SMT solvers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6039408$C803C325-1B4C-4EFD-8C3A-C448DA2C317E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"fe6dc588442db2cdc230ae5a66e7dda4ed6e50c8","datavalue":{"value":"1511.68259","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6039408$76D32B73-6633-4623-B613-2740B5597142","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ee96e73c9e014af7bbb7d5caf75a5bf42e6ee362","datavalue":{"value":"10.1007/978-3-319-96142-2_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6039408$F770D962-A15C-4B46-823D-83C5C322FC9E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7749ea419a7c3b783242f22f32dec4d05237622f","datavalue":{"value":{"entity-type":"item","numeric-id":2040599,"id":"Q2040599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6039408$3583CA9F-D53D-4B57-A785-EFC7FB3373B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d33dbcf1c53e85929fe28108a0d752643d16a11","datavalue":{"value":{"entity-type":"item","numeric-id":1412836,"id":"Q1412836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6039408$1A26CF72-FFB4-4DB4-9E6D-651179E2E4DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"50100327a2c6f555e4a4810ba0263aa80d7a14ed","datavalue":{"value":{"entity-type":"item","numeric-id":526761,"id":"Q526761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6039408$6F509C7C-6E63-4717-B131-BC4533E8718A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d4ba228bb5693c2e3eb7592c46c7d713183c8c65","datavalue":{"value":{"entity-type":"item","numeric-id":2864836,"id":"Q2864836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6039408$1B66FBDF-7DD5-42C3-ABA5-F2B85180D468","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5a9ffdd3d0278110160d03bdc1ac988576aaeda7","datavalue":{"value":{"time":"+2023-05-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":"Q6039408$10736F02-9C6B-4980-8E5E-E4222C75F033","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6039408$D358CAC6-8F20-4A86-8616-47BE8315D6CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6039408$1F353E25-C15B-4FC3-93D1-D6838DF4A9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6039408$1A6CECF5-5C54-4B13-9DE7-D728D8C5B42C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a09a4a961964ed698e15596e69c535b6b4e947ad","datavalue":{"value":"7682383","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6039408$A3C0B9A8-6052-4883-A330-5800C484EAD8","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":"Q6039408$2DE41D39-A136-4D0D-85E0-0C1D796F0975","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a102b4299cdcd1142dc21044f6b7447c46cf4292","datavalue":{"value":{"entity-type":"item","numeric-id":543613,"id":"Q543613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b26d847218a3da4d10f56e63bac35ad65673a9b","datavalue":{"value":{"amount":"+0.8008596301078796","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":"Q6039408$2D2EBB72-1245-4DBE-A202-B3B0C35D5D19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d68b24b1168f9d47fac5c9e15376f715e582492","datavalue":{"value":{"entity-type":"item","numeric-id":2908473,"id":"Q2908473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b1a0c1257fdebbadbcb2e804c339462c204d4209","datavalue":{"value":{"amount":"+0.7471104860305786","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":"Q6039408$9A6D2999-78F5-4833-90C9-5C17F9DAFE2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20be01fbf4b31a6c572813f122c9731cf8ec03c9","datavalue":{"value":{"entity-type":"item","numeric-id":3192050,"id":"Q3192050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7d439b5606110026e84fe6d5b7d06a18a67e5d5","datavalue":{"value":{"amount":"+0.74484783411026","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":"Q6039408$29192AB3-BE4D-47AD-AA7F-BFCB72552B16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd916d873ee39f0fd3bb37ca98a6b886fe5da0a6","datavalue":{"value":{"entity-type":"item","numeric-id":2661344,"id":"Q2661344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f240377075b4342b74e9c61c4ab5fda47cb773c6","datavalue":{"value":{"amount":"+0.7442546486854553","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":"Q6039408$5D1F1AE1-7E33-49D2-A7CD-2C4946217611","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e67fea2f956732ad9563fafc976c7b9b74d842c","datavalue":{"value":{"entity-type":"item","numeric-id":1799112,"id":"Q1799112"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0ad4fc0cd10ee2b0027bbc841c64b2cb6049d49b","datavalue":{"value":{"amount":"+0.7439281940460205","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":"Q6039408$0A974B9A-2043-44F6-82BC-1994B8374F22","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6039408","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6039408"}}}}}