{"entities":{"Q2280222":{"pageid":2290965,"ns":120,"title":"Item:Q2280222","lastrevid":73028706,"modified":"2026-04-14T09:30:33Z","type":"item","id":"Q2280222","labels":{"en":{"language":"en","value":"Refutation-based synthesis in SMT"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7144324"}},"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":"Q2280222$D22BBF3F-9B8D-4367-80EB-397CB71C3DAC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"132356b0f70d74f1dc6c7ec11fe10040337c80b1","datavalue":{"value":{"text":"Refutation-based synthesis in SMT","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2280222$5479BE81-E95B-4C2E-939C-63D143EB5FFB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d4827e28a674d8237a8bbb1d3decf50a9860c09b","datavalue":{"value":"1427.68051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280222$7A07EBD0-5B07-44C6-A77A-C941992E1AB3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"84952d23570c02a49b2cbd6b6731071617699380","datavalue":{"value":{"entity-type":"item","numeric-id":518398,"id":"Q518398"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$11737A5E-FA21-4D66-8B6E-0833D9A2AA7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"947e5398223830d4c80e75386dbd3c8e6dd67f1d","datavalue":{"value":{"entity-type":"item","numeric-id":429585,"id":"Q429585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$2AB0BEF2-C7F3-4E60-9552-2EA947461936","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad77f9f95b13763d1bf3e18f3ef5b6900b795f74","datavalue":{"value":{"entity-type":"item","numeric-id":518400,"id":"Q518400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$F442E224-9A54-4954-8B20-8204D1049A7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5374aaae6c4fa00723de88e8acb31ca46f3aaf1e","datavalue":{"value":{"entity-type":"item","numeric-id":518401,"id":"Q518401"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$A2740D5E-DB25-4A90-9AC9-3092EB4D9CFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9c4a981688ce96064434c07429a9f8191c6df21c","datavalue":{"value":{"entity-type":"item","numeric-id":746766,"id":"Q746766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$D19DF75D-9DFF-4D4B-A28E-352E3BBFE622","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$A28EABB6-4EF7-4C20-A96F-CBC12AFCB054","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2f6772b50db402e319131e91836e24f594dd3ca2","datavalue":{"value":{"time":"+2019-12-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2280222$6677920D-F693-4F9D-B60A-AA30F779855D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280222$5CCAF30D-6440-4DA1-AE43-B7CB1EF5003A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280222$5F2D123D-4529-40ED-ACE3-4B119F0CF685","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"704fe2cdba786af27dcd28b38e3bf49dd8fe6c4c","datavalue":{"value":"7144324","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280222$F8696E57-DDD2-406C-B01E-099863AE2BC9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4518906703ac547f79888d08670823c3951a15da","datavalue":{"value":"program synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280222$77C5053F-B9AE-44E4-A8CE-433BC5899579","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1254a7c01d2970b87da2854c1fde40c268a1f55d","datavalue":{"value":"satisfiability modulo theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280222$E382F143-95E4-49BA-B6E5-C771E0E400E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a20a062630d1bb5cf9aa5d669cd08fbd3eee7671","datavalue":{"value":"automated deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2280222$5CB0677B-CEEE-4E45-8C9D-F5FE08E6438B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa0d89c0a8d281cca595eba1f33ef7e0ef5464ab","datavalue":{"value":{"entity-type":"item","numeric-id":54038,"id":"Q54038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$F84EA93C-AC09-4446-8E96-901A56EC5302","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2822825cdea331aa7c0ec2c340c1eb36d62db00b","datavalue":{"value":{"entity-type":"item","numeric-id":17123,"id":"Q17123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$5565DA65-BA41-4389-95B9-ED61C6A805C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$5A53BDE2-F3D6-4B9F-B295-CE12A4F32D82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"45fa147ad24d78ff9111165d21eddec7203c8bfd","datavalue":{"value":{"entity-type":"item","numeric-id":20838,"id":"Q20838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$716FE216-BF62-4228-A496-AE71907B5FEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f977d90147989768e21daaa75bb9e675b4c21143","datavalue":{"value":{"entity-type":"item","numeric-id":5973448,"id":"Q5973448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$DEC54AF3-99C4-444F-9ED6-178663E34CF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"85575b60ef4d0a8413d3c895be2530b8915bc3fb","datavalue":{"value":{"entity-type":"item","numeric-id":16612,"id":"Q16612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$09883336-8DEB-4C18-8B8B-261BBA88EE6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$CAB21E7B-78F5-476E-BB88-C54125C8B9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"549148d32f0439e7b014790e18353e555528aa0a","datavalue":{"value":{"entity-type":"item","numeric-id":31323,"id":"Q31323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$1401CA13-AECB-4626-83E4-E3759DE2B72E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bd3fa568ce44545ce1c1bded3c45ecc37b43b7c1","datavalue":{"value":{"entity-type":"item","numeric-id":21467,"id":"Q21467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$2D8A12B4-C504-4571-A554-B58EDE396549","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fd1f11f1c714006456b4bd54bab92a11b4a8c134","datavalue":{"value":{"entity-type":"item","numeric-id":40388,"id":"Q40388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$1D2B8B3E-C8D5-41AD-A15C-AB595507C7E5","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":"Q2280222$C94BFBF3-2270-41AE-BAFF-EDE2F6E9C4DA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7b505d4bc22e60ebe8a7ee157f3c75a7f6fb44a6","datavalue":{"value":"https://doi.org/10.1007/s10703-017-0270-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q2280222$1CBB02FA-0C5B-402B-A10C-F2FDD7E245B3","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"50a8984b38a939b3c49e74683fff41887b6c861d","datavalue":{"value":"W2589084440","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280222$123988E6-5A8B-40A6-8622-819103BA6C85","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6820d466f20a132975882100c6125897eef0f140","datavalue":{"value":{"entity-type":"item","numeric-id":5309032,"id":"Q5309032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$3D904BF2-57C3-4A17-8086-A86F0695FC1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26c01bfb65f437d69fdbcfb2d9f8c34823e70739","datavalue":{"value":{"entity-type":"item","numeric-id":5747770,"id":"Q5747770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$9C1661B5-AD82-47DC-A5B6-1774F9EE21DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6af1feed9420fbd9bfd80527390996ecd04d3fa9","datavalue":{"value":{"entity-type":"item","numeric-id":439954,"id":"Q439954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$F9D7D491-D696-41B2-8091-941B4076AFF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3cca9f9428ea63e6117d5a41c3da120c355291ed","datavalue":{"value":{"entity-type":"item","numeric-id":5711486,"id":"Q5711486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$7FD1DC95-3684-4BBD-AA1C-896EA6C3A79C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9422da50d2a3eee12c5b953358d4af4d314c375","datavalue":{"value":{"entity-type":"item","numeric-id":5200027,"id":"Q5200027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$352D32DF-091D-42EC-A37B-2F58CFB1BFF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1daf6c1b27d4e2241acccb436e068cfc4f24ffff","datavalue":{"value":{"entity-type":"item","numeric-id":3546294,"id":"Q3546294"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$9AE95B8C-CCC4-4A24-9A43-C6A11BCD0E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d425524c539f34b2c20b8cfec23a758c1eb81a6","datavalue":{"value":{"entity-type":"item","numeric-id":3608772,"id":"Q3608772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$82E56B84-9D7B-4209-B499-41D6662CF40D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f426d61b5e73f09c762af22502a76e1d6d446b2d","datavalue":{"value":{"entity-type":"item","numeric-id":3636870,"id":"Q3636870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$7DFB2A5A-DCF1-4977-8DEC-8FA73D64F389","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"620e4e63cec9d7a183b3bc9b7082cb1e2f14d371","datavalue":{"value":{"entity-type":"item","numeric-id":3075488,"id":"Q3075488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$A5D73FD3-9D68-40BF-AB1D-5DCE2752DE9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"330ce073a559eb014c24d439e8bed6879ab9c0af","datavalue":{"value":{"entity-type":"item","numeric-id":2843327,"id":"Q2843327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$9DDA2B20-FEF8-4712-AB18-6D1162C320DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3686a074c7686604cdf852bc86af741c152a6f8a","datavalue":{"value":{"entity-type":"item","numeric-id":3007686,"id":"Q3007686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$224AE108-B8B7-4384-B6B6-039BE39B3953","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1060c39f6c78c6c906f6922c72b026efa0999e0","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$2B66AD05-8218-48B7-AABB-33ECEC975E8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c77dc933c73e4695de7ff6375817b86b37737aa","datavalue":{"value":{"entity-type":"item","numeric-id":3922132,"id":"Q3922132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$396E5D4C-21CE-408F-9323-5820F9E9212C","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":"Q2280222$47D4BA34-0C84-4CE6-99F4-E4B85CF031C4","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":"Q2280222$14DBDDBB-AD47-4CE5-8245-94040AEC6044","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0100b938aa02592e3dcec5a016d883a9d79cc50a","datavalue":{"value":{"entity-type":"item","numeric-id":4205072,"id":"Q4205072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$5EDF7667-68E6-444B-BAEC-C2AFCBCB555A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4bf82aa5c825000208c5b437043a5cc9fbc4323","datavalue":{"value":{"entity-type":"item","numeric-id":1702893,"id":"Q1702893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$9D11F418-71E4-44DB-B7CB-F5C05CA44E5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d3f5b196c0df4a4076dad9269fa5296f4cdaaab","datavalue":{"value":{"entity-type":"item","numeric-id":1688537,"id":"Q1688537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$17E1893F-F2FE-4C77-A844-4DE4D8091B74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"197bd6d0b9b13f7d7d62b39ca988dbf1f2dfc0db","datavalue":{"value":{"entity-type":"item","numeric-id":4928453,"id":"Q4928453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$9563C160-1DB6-4EBD-AFAD-4485458EB807","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bda1299c2c035b74ffa695f3cdd7ba8cb218b33","datavalue":{"value":{"entity-type":"item","numeric-id":3454117,"id":"Q3454117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$86AAB4BE-DB53-44A4-95E9-8F6BDB6D262E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48af5adf09c22725f6f724fe9db0206a76af8fd0","datavalue":{"value":{"entity-type":"item","numeric-id":5464658,"id":"Q5464658"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$7342B17E-4F37-4DB6-96E3-668D8D083BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1cf1fbb097a93619e873e24271fa9638a00cf8d","datavalue":{"value":{"entity-type":"item","numeric-id":2441770,"id":"Q2441770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2280222$2C50DE55-D7AC-4A7E-82AB-6D190716B4B6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"13c9d6993a9c460e68278f690685588891d5aef3","datavalue":{"value":"10.1007/S10703-017-0270-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2280222$C1C613D1-A9F0-4960-9C58-7A26E05DC213","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81fb1657427495232c5ae2608a0e6d15ca998a89","datavalue":{"value":{"entity-type":"item","numeric-id":1702893,"id":"Q1702893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ddb3370c22bdc769f1706e64a8b484ed4ff33ef1","datavalue":{"value":{"amount":"+0.9304112195968628","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":"Q2280222$162B4BDD-B305-4924-8B5D-94613D0FD44A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a01942a02711b00fe4d9ca41ae8b4ea9eaaf7d6","datavalue":{"value":{"entity-type":"item","numeric-id":6045008,"id":"Q6045008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb045304372692bc4d970f05bea262e18c9d6b47","datavalue":{"value":{"amount":"+0.779923141002655","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":"Q2280222$670A4FF3-814A-4448-9196-06A4027C4CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5286bf29d1aaa2124996c5dbc7629f045b4580ef","datavalue":{"value":{"entity-type":"item","numeric-id":2152655,"id":"Q2152655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"886def5f419578d84005d39de47923a44faf3678","datavalue":{"value":{"amount":"+0.7734176516532898","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":"Q2280222$F3563F08-32F9-4656-847C-31210F42FD35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97bd5ab765d1851261b0bfadc8d534c87a3dcc72","datavalue":{"value":{"entity-type":"item","numeric-id":5255085,"id":"Q5255085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"650d499cdfeac1d0271d5839bbaaf07092ee610c","datavalue":{"value":{"amount":"+0.7614645957946777","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":"Q2280222$26C00222-8F76-44BA-B347-8A52EB132869","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"33be3ca80d76308be4e7e250be0c28a168d52563","datavalue":{"value":{"entity-type":"item","numeric-id":2181939,"id":"Q2181939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e84ab18b134ba92054d36ef64ba710b1c40052dc","datavalue":{"value":{"amount":"+0.7572622895240784","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":"Q2280222$76822ADD-54AF-43C2-B40D-4D086FBEF6E9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Refutation-based synthesis in SMT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Refutation-based_synthesis_in_SMT"}}}}}