{"entities":{"Q2209549":{"pageid":2220292,"ns":120,"title":"Item:Q2209549","lastrevid":71553264,"modified":"2026-04-13T23:01:14Z","type":"item","id":"Q2209549","labels":{"en":{"language":"en","value":"Efficient strategies for CEGAR-based model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7268894"}},"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":"Q2209549$F0BD2398-37C2-4925-A1B2-19A2B9683D40","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5432e09759b163d6fd603e5bf2185bcf4fbbe083","datavalue":{"value":{"text":"Efficient strategies for CEGAR-based model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2209549$7BDB0B8E-146E-4DFD-AE30-0A97AF1033C3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5e6ca3e8b0910ad2f93534d546cfac3f100a5ad9","datavalue":{"value":"1468.68131","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2209549$0B09389F-3830-48A0-BB7D-93322AB8907F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d55ed1eccf0c74033df0ea1863e30c55258a672","datavalue":{"value":{"entity-type":"item","numeric-id":2209547,"id":"Q2209547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$486709D1-7D45-49E0-910E-8223170DB1B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f061b5963c8cce3a4689273d601a2ddcce9285a","datavalue":{"value":{"entity-type":"item","numeric-id":2209548,"id":"Q2209548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$EDC78187-00CC-42E9-9C34-2665CF40B46B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$8FE23F66-09F7-419C-8EC3-FD182E7C0778","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4011c0437b0c50916bbdc1f2b0514a4c041c71e0","datavalue":{"value":{"time":"+2020-11-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2209549$1BDE1AC8-5279-4994-8C15-9A5C826FD95F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2209549$687C2CCF-3024-4598-AAC7-E7767127A3E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2209549$46C7C8C1-E9D2-429B-A012-1308D56AE911","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3d897fd7da017de8bf78088846f2d33f03a7dcc9","datavalue":{"value":"7268894","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2209549$283F700E-0FC2-4C09-AA36-E290B327C8E3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2209549$7DB48CD6-4F8D-4F71-B37F-1A2EC34F421D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e404e0d47002bfb1532cb42cfe324606a2151619","datavalue":{"value":"abstraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2209549$FD0D8E93-11C0-4839-934F-E3EAE9AC5F1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae8794be5634259987f7e3035390d183ba5b4edb","datavalue":{"value":"CEGAR","type":"string"},"datatype":"string"},"type":"statement","id":"Q2209549$C647A13D-12BF-4190-802C-73E9D7C5FAC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3152daca964c287d63a0126bd987834e7cef4476","datavalue":{"value":"experimental evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q2209549$8C37B704-E1CD-44E7-A146-F3D05E4A91B1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b2f45492d0a9ee38c7f6f7ea29a7881599069d9b","datavalue":{"value":{"entity-type":"item","numeric-id":13519,"id":"Q13519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$621F4166-300C-46E0-8EBC-160B3F326327","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"95971f6b611ca7d919754c769fae0e473be28779","datavalue":{"value":{"entity-type":"item","numeric-id":19265,"id":"Q19265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$587A34AB-1BEF-4A36-B2B8-E3318D3A691E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2c47fe2df1f1953bad823a45d5770cd3dadc8780","datavalue":{"value":{"entity-type":"item","numeric-id":19438,"id":"Q19438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$DA5F3522-4CE2-4A29-9CAE-DC3B8CB93291","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c7107a3607349765606fad319a8423745e29c6d1","datavalue":{"value":{"entity-type":"item","numeric-id":24728,"id":"Q24728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$5E844096-0E21-4AD3-8F0E-F37051B54F10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b3ad9fce9060c14f348316440256eb8b089be466","datavalue":{"value":{"entity-type":"item","numeric-id":26383,"id":"Q26383"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$953C58E8-22B8-4939-8195-394C8099BB24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3fa0ba30f2225a69a75d233361703cec68c39010","datavalue":{"value":{"entity-type":"item","numeric-id":15473,"id":"Q15473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$AC2D9DE4-08AD-4185-B986-90DA2F4189C6","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":"Q2209549$C84D7DE7-CD4B-4A48-AA3A-2AE19D7F3E6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a1d6b9e920f2e41a66a9767e31ca972ed7628dde","datavalue":{"value":{"entity-type":"item","numeric-id":15668,"id":"Q15668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$8070BF6F-F57B-427E-8A55-38D03B2C859B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d5dcb486ea2ffc39531287854f4a7be9ffb011b4","datavalue":{"value":{"entity-type":"item","numeric-id":17045,"id":"Q17045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$9E0928E1-E52B-4D52-AF87-612335DD35C1","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":"Q2209549$1DEDA704-D0AE-4590-ACDC-F1AAAC7CD5C1","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":"Q2209549$3B22F71E-D550-44B7-B0D5-98BE1DDEE710","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":"Q2209549$F8B2A519-D2FA-4816-99F0-0DD61740D45B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe309b34de2508c6ceb3eb2072d8c6bce447a5de","datavalue":{"value":"https://doi.org/10.1007/s10817-019-09535-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q2209549$CEC0498E-64CF-4292-BD28-14A6884F2899","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ff554531c93a6d1d6ee5380ef68155d1136ce712","datavalue":{"value":"W2988671542","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2209549$ADE1590E-0DC2-4401-9E46-8A13ADA91DE7","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"530d4ed6d0f32858e402afd6be6ad7fdf028444e","datavalue":{"value":{"entity-type":"item","numeric-id":479820,"id":"Q479820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$9748944E-7C2F-4CB3-B008-AEE8FE8DA464","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dbd5e9b7224b44a5be727c6870f16a737b8c3625","datavalue":{"value":{"entity-type":"item","numeric-id":2769592,"id":"Q2769592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$AB8370C3-A2AC-4097-98B9-CA69D4D6DB35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22fbdead51b7f0506fece1b77dbe9fd8703e32e8","datavalue":{"value":{"entity-type":"item","numeric-id":4553257,"id":"Q4553257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$1C23E337-D2C3-4E93-9B09-D29D3F3447F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e94cba08ae745a177d77c1491f4f47f8e7dfaf89","datavalue":{"value":{"entity-type":"item","numeric-id":593176,"id":"Q593176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$7A5600A5-1A0E-4878-A3F7-C31403DE4590","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc25af5045c856aadb22057606de79dc70eaee2","datavalue":{"value":{"entity-type":"item","numeric-id":1703012,"id":"Q1703012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$DF191ACB-F3F1-4C7C-87E6-2B158BBFE1DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad7f4489d4c89d794424e5e3872c38fe58d4c967","datavalue":{"value":{"entity-type":"item","numeric-id":5429342,"id":"Q5429342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$E463A771-787F-4DA3-9505-0F315E687E82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f814032017aa40390d4c6f26a550d62bb08ff374","datavalue":{"value":{"entity-type":"item","numeric-id":5503674,"id":"Q5503674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$66D33618-ECBD-4600-8ACC-1E19CB313F1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64edbd4b0368a46cc24983dcdc802e4982142495","datavalue":{"value":{"entity-type":"item","numeric-id":5310200,"id":"Q5310200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$7A3245BB-88AF-4071-9631-48A1F614D83C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6be745c1e3c92f55b154456d6a9b2f6da7bdd3c7","datavalue":{"value":{"entity-type":"item","numeric-id":3508510,"id":"Q3508510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$74247F4D-CE07-42B8-95A7-C8326AC39578","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b026130fb14abb6ec25af9a49779c945ecc8f0fd","datavalue":{"value":{"entity-type":"item","numeric-id":3452508,"id":"Q3452508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$F228286D-8E6D-4574-BD56-9C093341C520","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a768592a36a0799f3311c6c16dd9cd5a4a03baf","datavalue":{"value":{"entity-type":"item","numeric-id":5703792,"id":"Q5703792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$626FAEBA-3405-4DA4-80B8-1CE4D3600769","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26efd78e544357dc906756a8cde9d92440028650","datavalue":{"value":{"entity-type":"item","numeric-id":526771,"id":"Q526771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$0E174527-1CFF-4266-BAEB-6F53567BB649","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c0c766394f5e5ce0b65882d3a1a29dff11575f5","datavalue":{"value":{"entity-type":"item","numeric-id":2891411,"id":"Q2891411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$A8A96905-9AA4-4EC6-8EB9-C87426F11C87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72453431b10b3f97c51f820a77b59fa085fa0127","datavalue":{"value":{"entity-type":"item","numeric-id":2827465,"id":"Q2827465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$88A877AD-5CF6-46F7-8DA0-313BA875B8B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4e94238a6a5ddf3dd15f03313efac1f027d9611","datavalue":{"value":{"entity-type":"item","numeric-id":3452263,"id":"Q3452263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$B10DAFFA-C49C-4846-A664-5F4872DC5A03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91c21e537ab0c07b0d3849b9a7e5a291ced75540","datavalue":{"value":{"entity-type":"item","numeric-id":5178898,"id":"Q5178898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$DDE2DEEA-F4A7-42EB-9525-5416BDA317CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e29a9e63db651327a88d88e2cdc75e51e9cd4afb","datavalue":{"value":{"entity-type":"item","numeric-id":2843329,"id":"Q2843329"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$B8E7793E-E7A3-4C05-A8EB-093991698917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f54bc0e2f92beb50e9c6902664de23aa76daffd","datavalue":{"value":{"entity-type":"item","numeric-id":5703754,"id":"Q5703754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$0B90FA1B-4C41-42A1-8B5B-3AC4E43DF06D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2d9d5673d377c95422809e446c2052b58cca8ec","datavalue":{"value":{"entity-type":"item","numeric-id":5756749,"id":"Q5756749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$9957BCA7-C076-4F3E-959A-66DE2CDBEDD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"171f2f23484cc563361b9a949250d7cf0cf0889e","datavalue":{"value":{"entity-type":"item","numeric-id":2479551,"id":"Q2479551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$0D03D886-EBDB-4ADE-88B6-BB795BE4125A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cbe2b7ace5b154d5b637e4b04023a9a701221e7","datavalue":{"value":{"entity-type":"item","numeric-id":5883582,"id":"Q5883582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$57DF5DEE-7EFB-47DC-B625-7F909FBBFBF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11d88d9031b6f83724f098b2a452ecef52fee53c","datavalue":{"value":{"entity-type":"item","numeric-id":4672991,"id":"Q4672991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$200F1963-9D08-43FF-9118-7BBD91A546E8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f86eadca1e2c392d568e44433e07b0cd6e326931","datavalue":{"value":"10.1007/S10817-019-09535-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2209549$7741B93B-09BB-4F9D-85A3-14A67327089D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a1385e9d56cd5ab23b7515280fe8bcfee106954","datavalue":{"value":{"entity-type":"item","numeric-id":2827465,"id":"Q2827465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"421653ff10e89d4a7d3e148243413827a42f2a6c","datavalue":{"value":{"amount":"+0.7770788073539734","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":"Q2209549$C7C33F61-7D48-4481-AA64-E58B7464748E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b9fc369e46fc329463fea3bac110c1110bcfcc7","datavalue":{"value":{"entity-type":"item","numeric-id":5716541,"id":"Q5716541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aeb6568d06a83258627bd8172a0aa21242b091e7","datavalue":{"value":{"amount":"+0.7607428431510925","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":"Q2209549$B2DF8CD0-DDA7-49D7-92A6-E29800556B66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d3eab57d91a654c4eadcc66da4fb3257585003c","datavalue":{"value":{"entity-type":"item","numeric-id":4738460,"id":"Q4738460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a82bdf811013881aea63c0c98ea1be265f01ff90","datavalue":{"value":{"amount":"+0.7352603673934937","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":"Q2209549$5B205933-D4E7-4D82-A485-DEFB6B9BD128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65fd47484c6b00d882d3302f057fc283b851b47a","datavalue":{"value":{"entity-type":"item","numeric-id":4930739,"id":"Q4930739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59400022f39bafb7b77a31f455f47d1a62f1c9de","datavalue":{"value":{"amount":"+0.7342876195907593","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":"Q2209549$899C8386-F4BC-486D-85C1-033489C768E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"729cef116b6290fc31462f3f9f3e3f41f50f616f","datavalue":{"value":{"entity-type":"item","numeric-id":6487321,"id":"Q6487321"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8def2577e235697cd9e8c9dfc0201e32cd7e1745","datavalue":{"value":{"amount":"+0.729000449180603","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":"Q2209549$170948A0-8F8F-4CA5-BBCA-A3AEFCB0CEA6","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2209549$54276C14-ED9A-4F97-86ED-1EF8A5E98943","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient strategies for CEGAR-based model checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Efficient_strategies_for_CEGAR-based_model_checking"}}}}}