{"entities":{"Q5256336":{"pageid":7285904,"ns":120,"title":"Item:Q5256336","lastrevid":91966343,"modified":"2026-06-05T00:31:35Z","type":"item","id":"Q5256336","labels":{"en":{"language":"en","value":"Modal Satisfiability via SMT Solving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6448703"}},"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":"Q5256336$9F53F93A-DAE9-4469-B561-A05C1669D62E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"650cbed423ca0a5ca972fdf55ec71ac6972b8985","datavalue":{"value":{"text":"Modal Satisfiability via SMT Solving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5256336$B41064E5-6541-49C5-95F4-A5E1068FBCEC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e43325d75a88db8f3f7a592869efc8e2a48d715e","datavalue":{"value":"1453.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$3B27E2C0-8B13-4640-B4E5-D575A10927CB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"af42bfac79e457687c81f42ab5ba3d439c593266","datavalue":{"value":"10.1007/978-3-319-15545-6_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$E8AEC3EB-16B3-45D7-90DC-84AD57527118","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"daef4e411daa48c61f34c5e5041ae1e9c70ed42c","datavalue":{"value":{"entity-type":"item","numeric-id":190282,"id":"Q190282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$29940D89-EA63-4B61-ABBD-862B97B20955","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"17d182828bb3dd01cff9766a0bb3efe1eeb4424b","datavalue":{"value":{"entity-type":"item","numeric-id":436375,"id":"Q436375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$477B2131-F575-421F-BB26-4323AE01C5FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5a4b473513180cf93e4a8c86844a2c4dad9ce336","datavalue":{"value":{"entity-type":"item","numeric-id":820130,"id":"Q820130"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$15251039-30C4-448F-B6F3-32746E8B5055","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c5e0fb570f569e128c7aaa0023b42f1ff2ef5c78","datavalue":{"value":{"entity-type":"item","numeric-id":5256327,"id":"Q5256327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$4E53D7FC-5037-474B-9E6E-B6C4BB76077F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c80eedd2756b3c5cb35bb218ffa4134f7861c0b9","datavalue":{"value":{"time":"+2015-06-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5256336$D715ED31-B4DD-44D3-8EBA-928D55AE0FDA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a8fbd1d69fd9fdcff1f12d7dd7b778bfa4695f5d","datavalue":{"value":"https://hal.inria.fr/hal-01127966/file/main.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5256336$CC34691B-2B75-4CF8-A36B-52BCBBDE43F2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$81341A1A-803F-4732-B7C4-581E302D8F71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$25F947D2-725A-4B1E-8EDB-EE40F7407C1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$1EDE99E9-341C-40DD-BEDD-D71A1ED6B34F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"630c0d4968ab768eda0c399a67492907d42f6803","datavalue":{"value":"6448703","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$266CF5CE-FEBA-4DCA-BD2E-C15AE69D8E94","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":"Q5256336$3FA79D7C-9B3F-4095-A208-FC1DB288A56E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fcd2582a8cb936529a8378f78dff1accf05aff3d","datavalue":{"value":"W2110715144","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5256336$064EFD91-23AC-40F3-AAD9-02A119AD8B90","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a49b20b1506647b1c87e6ed6310fb943dc6407f8","datavalue":{"value":{"entity-type":"item","numeric-id":1267082,"id":"Q1267082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$F6749630-B21E-438E-BBB1-9C42EDD48B25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7fee338715b5fbfcfe3ffbeb0c47dcbe3630167d","datavalue":{"value":{"entity-type":"item","numeric-id":3999578,"id":"Q3999578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$B3F2BB44-AAE1-4D8F-84AA-5FE7F4BB3D8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adc87194f53a9552766b22cbe3fffae4e25dcae6","datavalue":{"value":{"entity-type":"item","numeric-id":2744124,"id":"Q2744124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$64A89E3D-BB35-4ACC-A439-A9020247BF56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a434d8d83635d48a94c51e468983008bba00fd2a","datavalue":{"value":{"entity-type":"item","numeric-id":5431611,"id":"Q5431611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$B4410867-A649-49C2-8DFB-2908550EDA18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af4555c0d89e243a8a9351cedc1b4ffbfceace09","datavalue":{"value":{"entity-type":"item","numeric-id":5691140,"id":"Q5691140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$C5C3DDED-2930-4AB8-8887-9F1346236898","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75b2763e4a26f45c3f780a824c58a0cce849a254","datavalue":{"value":{"entity-type":"item","numeric-id":4329239,"id":"Q4329239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$D8A8709E-CC62-4BE2-B223-B3AA4469B7A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"153ff2c071bc5db7ed2a4a4864b90953ca620982","datavalue":{"value":{"entity-type":"item","numeric-id":1854375,"id":"Q1854375"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$9FD484FE-1DEB-49D7-BA11-65E02DE6E8FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04c95b2120f2667fd164e113196945ce09600483","datavalue":{"value":{"entity-type":"item","numeric-id":4007156,"id":"Q4007156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$868A444C-7D5D-4968-B0E2-96758A8516F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"706ea3dccba515a44c5b040176691d86b72d5b5e","datavalue":{"value":{"entity-type":"item","numeric-id":4266483,"id":"Q4266483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$1967A118-E183-4B0A-944E-E64ACBB8090D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b19d4c961176e9452dd55fdddf2406cd05d35f5f","datavalue":{"value":{"entity-type":"item","numeric-id":4338040,"id":"Q4338040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$63BC02DE-929B-453D-A08F-0A9F0784D05A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec26365896126f6bfdbaf8332a7af025cdb680e9","datavalue":{"value":{"entity-type":"item","numeric-id":4487263,"id":"Q4487263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$4B6E1283-0CDC-409F-85DD-D63295817580","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$2453F2C3-4423-4160-8D13-7EAF01BCEC9F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d5db726edf837519cac147ea3a710fea1c2fa91","datavalue":{"value":{"entity-type":"item","numeric-id":4365320,"id":"Q4365320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$A55E0959-131B-47A3-9CF3-D6C3B48B235E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6579ba18a64bfb68d3585281c63df9817611aced","datavalue":{"value":{"entity-type":"item","numeric-id":4916086,"id":"Q4916086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$1ADE6E1C-BEF0-4C78-9950-C7F79FD151AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"32ed882b3979db3c64d5bf182ed038c035ede3c3","datavalue":{"value":{"entity-type":"item","numeric-id":5410334,"id":"Q5410334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$F7776AF9-DAB0-4CD5-8445-9B30646C1ECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1613a6ff5ac7b010de5ba58e55ebd9cdec3d5273","datavalue":{"value":{"entity-type":"item","numeric-id":5765445,"id":"Q5765445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$A0507016-3DD8-4E78-8578-0FF2F1AEE1AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b90ce7fe73f733b88d2da3dac92118f16962252","datavalue":{"value":{"entity-type":"item","numeric-id":4353561,"id":"Q4353561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5256336$7A33A5F7-102A-49FF-B2E7-277007D10FDC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d343104e13ebed7dbcd78ce1d8780b01a8c06605","datavalue":{"value":{"entity-type":"item","numeric-id":1759682,"id":"Q1759682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33379402ecd150033a0cf54de10f9392fdd92bbc","datavalue":{"value":{"amount":"+0.9370542","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$A07451EF-6C75-472C-A78B-221AAF8B6BAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8be3561be537242c940a508facc3d798e41c46d","datavalue":{"value":{"entity-type":"item","numeric-id":3587453,"id":"Q3587453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33379402ecd150033a0cf54de10f9392fdd92bbc","datavalue":{"value":{"amount":"+0.9370542","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$77F76E6B-968F-43CE-9FA7-F6E6136526DE","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":"0f1fcd2d90407732dbc7f57481738690996fd917","datavalue":{"value":{"amount":"+0.93406177","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$325B495E-6611-479F-AE75-0B72972E7FEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353b46cb2a124cc2200384a940b087517c5b273c","datavalue":{"value":{"entity-type":"item","numeric-id":1037239,"id":"Q1037239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"72502071b132a10292331f9f34cc512cc0af2a6e","datavalue":{"value":{"amount":"+0.9193934","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$BCAA5315-6252-4AAD-A32B-D6869F85F923","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a561bafa95356823f0ad6935cd5bde2996e23b7","datavalue":{"value":{"entity-type":"item","numeric-id":5901713,"id":"Q5901713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6eb504285ea068e555090089fa2ad75143742acc","datavalue":{"value":{"amount":"+0.91822624","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$BEE8C6D0-77F4-4272-A630-288A9EC53911","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":"b2449ddeb5d78d07a86ed772e407d8ea501f227c","datavalue":{"value":{"amount":"+0.9153613","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$CAD8EBE5-F8AC-42B3-8524-9930A76E7836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb29bdfd2432d520a44e436c9a9d449e487108e7","datavalue":{"value":{"entity-type":"item","numeric-id":2405239,"id":"Q2405239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"79cf784b014a7ce715392341af2755674e17ecff","datavalue":{"value":{"amount":"+0.91530335","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$B7EC0E99-F27C-4760-A661-7CF6BA65D5C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f568e93d54e2f02a5fe7ee1131eaf2b1ceb5e6c","datavalue":{"value":{"entity-type":"item","numeric-id":5019595,"id":"Q5019595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c519756f43562a8402f60c461014aec170dbb188","datavalue":{"value":{"amount":"+0.9152252","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$8493C761-BF26-41E4-BB71-CBA95DF63F0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f10ee01b04bf937ea18106e6d39f383b6936577b","datavalue":{"value":{"entity-type":"item","numeric-id":4931590,"id":"Q4931590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a9da1beb8ae0aaa7df90c1770a428ffd616f26ae","datavalue":{"value":{"amount":"+0.912143","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$554E9C35-2D84-47AD-869F-1AF5CD8B28F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4b46e267134ea318cd8e86042ef0a00b2e104f6","datavalue":{"value":{"entity-type":"item","numeric-id":988571,"id":"Q988571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88d35d88f04a08f7b2ce8d902f20c72cde630d02","datavalue":{"value":{"amount":"+0.91205466","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5256336$B5667B14-17CE-4FA5-B0CF-B0BA428A3E44","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Modal Satisfiability via SMT Solving","badges":[]}}}}}