{"entities":{"Q888467":{"pageid":890315,"ns":120,"title":"Item:Q888467","lastrevid":65219577,"modified":"2026-04-12T01:06:31Z","type":"item","id":"Q888467","labels":{"en":{"language":"en","value":"Optimization techniques for Craig interpolant compaction in unbounded model checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6502610"}},"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":"Q888467$BD740382-C74D-41D9-A979-C0AD45C802C3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0c991eadd6c00fdb643e35e6c838afb49501a788","datavalue":{"value":{"text":"Optimization techniques for Craig interpolant compaction in unbounded model checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q888467$622B0998-3862-465B-945C-A5E77A7EDA3D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f075de4613497a621968601e2aa17eb7b7a65171","datavalue":{"value":"1341.68117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$7B00DDEA-0E58-480E-B872-751E56551390","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"78ba453704ed3d872eb3c4e12877bf750b115031","datavalue":{"value":{"entity-type":"item","numeric-id":453481,"id":"Q453481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$437CD351-CCD6-4796-9CAE-46080F8AA675","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bbe11646b0ba55d8e784ea0ed5f362a7a08e59d2","datavalue":{"value":{"entity-type":"item","numeric-id":888465,"id":"Q888465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$374EA100-2718-4D20-8CC6-C05BB3950B96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"11c05bb91bf1988cc56a4d9fddcc880d553786ea","datavalue":{"value":{"entity-type":"item","numeric-id":888466,"id":"Q888466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$34B5A4CA-6C39-44E2-BFC8-C46D1706C00B","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":"Q888467$7A69F0A7-DA69-47BE-896E-20F94829E88A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fedb92f8006ce865a5ead1bfbb356102d7f9117a","datavalue":{"value":{"time":"+2015-10-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q888467$AA9394B4-7FCC-44A6-972B-344B898C2CFD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$35630AB5-89DB-4054-8814-060B06C51DD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c1d2d83da0d870574277144fdd1db9abaae162ec","datavalue":{"value":"03C40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$6FF85B30-A7F4-40EE-8010-A251077CADF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$C951AC27-E0C5-4F33-A767-77EFD55769FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1e903e68a16880f66ed79a0863889f1b2d3c837c","datavalue":{"value":"94C10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$B80E301D-68B6-479F-888C-C079FE9037E0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d6bf3553423a654c01a5f447f46e65ccbd735db7","datavalue":{"value":"6502610","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$7E68B0DA-AE35-4B95-ADDD-835BBB1986F9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"342e09d190155ca100024e455b49025512e8b20b","datavalue":{"value":"Craig interpolant","type":"string"},"datatype":"string"},"type":"statement","id":"Q888467$41E8843E-CDC2-4B42-AD0B-D6CB10FBBCA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"44398a47dcc646d236e796b5debaeb5832dfaa84","datavalue":{"value":"SAT-based unbounded model checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q888467$02696809-55AD-4275-9429-5539BD6F52B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fcab9163f53d6e5a171b7b1c65e7d87f375401bc","datavalue":{"value":"proof reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q888467$0E60DE61-F937-4716-9F45-F1A86E3257D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"45c0da7fdbd9e2ad03255453a71e4d2697cb02f1","datavalue":{"value":"interpolant reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q888467$0AC66053-5A80-47D4-87AB-39D19FF95BFC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ed66b4500809c164ad61ba9724c3cf07f26c2a82","datavalue":{"value":{"entity-type":"item","numeric-id":24833,"id":"Q24833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$FD8D673F-AD79-4E7F-B28A-382ACFF6449E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$CE8E21F7-A0B8-41E0-BCBB-D8C66F4FAC34","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":"Q888467$AFAA3CD0-4C94-407E-94C5-408B6D9A0898","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"69df6384e5f957a06e83581c17cca7995f262983","datavalue":{"value":"https://doi.org/10.1007/s10703-015-0229-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q888467$F9062A00-8CDB-488F-B117-4A74AC8EBA43","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e1465ec050b52ba80f0fc5ba0c2012af71a338b1","datavalue":{"value":"W2027979159","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$CC84C5AF-47E6-4C56-A0C5-F211C2FFDD82","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7de140db476e3cb4a77792caeebac28e6bb14357","datavalue":{"value":{"entity-type":"item","numeric-id":3244103,"id":"Q3244103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$344FFDCA-94F3-4F19-90C0-909C64819E2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d425f1dfe12ad30907606cc8a836303a30bbb11","datavalue":{"value":{"entity-type":"item","numeric-id":772220,"id":"Q772220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$4DC9104D-EB43-435C-A7A2-2688FF0FC3D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"348369ca3fccbe91226809a75cbf31afd7f3186d","datavalue":{"value":{"entity-type":"item","numeric-id":5900666,"id":"Q5900666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$EAD8643A-7CE2-4CC4-A23C-CBEA6191464E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef9a85754f10c794d7ea794155cce4bd2f066956","datavalue":{"value":{"entity-type":"item","numeric-id":3075471,"id":"Q3075471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$BD272B83-3320-4DDA-9DDD-79AB2E68F7F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af62bfd2162dabdadb1d68f1499174dc7482fad7","datavalue":{"value":{"entity-type":"item","numeric-id":5716597,"id":"Q5716597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$D32768E1-1553-40B7-87C2-88850D6A937D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62dd1223d29569eec68058706eac7eb8d1b02072","datavalue":{"value":{"entity-type":"item","numeric-id":5493247,"id":"Q5493247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$746777D5-8436-4B5D-AC0B-22B132B4A5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9bf74af701b8385747cfada5ecd2ea6d2b1e199","datavalue":{"value":{"entity-type":"item","numeric-id":5899061,"id":"Q5899061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$82403A06-E3AC-4481-8BBB-4956C8DE6047","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"263e0fb6c22c291ee04eddde59d9b3bb5516d5c8","datavalue":{"value":{"entity-type":"item","numeric-id":5452708,"id":"Q5452708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$2453286A-5059-4E94-82EF-1640DC527FCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$2E7C6BF1-3324-414A-97BE-E43A227CDD57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$5FA58985-705C-45BD-AF3F-04CDE66FCEA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f3dbc47deccb64d887f982dbe2cceb2d9bd9b1d","datavalue":{"value":{"entity-type":"item","numeric-id":5391528,"id":"Q5391528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$F674C336-0561-46A2-B7D3-E966A882FFFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b43a25ba24825d35a343ae255abd617023e5daad","datavalue":{"value":{"entity-type":"item","numeric-id":5200028,"id":"Q5200028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$90611082-790C-4141-93A2-0DF1994D6241","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"694c02ad293bfa66c9639e411421d6301f4d98c2","datavalue":{"value":{"entity-type":"item","numeric-id":4649291,"id":"Q4649291"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$8B64B52B-4735-49E5-96B1-FB2033438261","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7d6d6d217b399c1f6c096de595598b482d1f660","datavalue":{"value":{"entity-type":"item","numeric-id":4930598,"id":"Q4930598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$E8010D04-8727-4339-A8CD-90F0AC9B1037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cee1f5c4e596769f20c3e18240de0776d1bbf0f7","datavalue":{"value":{"entity-type":"item","numeric-id":4804900,"id":"Q4804900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$01629246-2983-4F96-9128-414E705EB700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"066fcf4f0ca79e30da3b6dde4a2b135c7aebd16e","datavalue":{"value":{"entity-type":"item","numeric-id":453484,"id":"Q453484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$A3837F2B-3CF3-4679-BA0D-6A454263D517","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a109c3ed51a56440af004e7f709b38f002714fd","datavalue":{"value":{"entity-type":"item","numeric-id":888467,"id":"Q888467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$3ECF1BFE-F9EE-4E4F-88D6-FC394DB2E97A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b4caf38d1ea0bcd43c14e944f03b1e72e20f485","datavalue":{"value":{"entity-type":"item","numeric-id":479815,"id":"Q479815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$888973F9-0DD0-431F-AACA-A0850D2EC5EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f015945aff3649e7842dc973c4e22842bcdd7d5","datavalue":{"value":{"entity-type":"item","numeric-id":2864838,"id":"Q2864838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$10A3BD07-6534-4A2A-80CD-4293FCE33A96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q888467$7B24FC0D-766F-42B3-8235-AD3D689A27BE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e8faefc4c36cc4581c61c1f98c5df52a6614fc76","datavalue":{"value":"10.1007/S10703-015-0229-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q888467$24DD4901-0C76-4BE2-BD11-BE641B8D9083","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f3e4418b90254da47f1e3ab57975e595d219a0be","datavalue":{"value":{"entity-type":"item","numeric-id":5899061,"id":"Q5899061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38e8a0880ff64add99080417e10eb6b91a5c7978","datavalue":{"value":{"amount":"+0.9017971","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":"Q888467$C6DC0E9E-902F-4A82-A3C2-4B64E8C80155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"761fca96bc8f5d7ed1a77087e8be1f0159097497","datavalue":{"value":{"entity-type":"item","numeric-id":5703754,"id":"Q5703754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"113d44f558ace857201a22357fde16ce85328b19","datavalue":{"value":{"amount":"+0.8937268","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":"Q888467$568D8223-84E9-4696-B316-ECB6B9AF8C33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a97945f30007bf4731ef6fa01728c84bec63d65","datavalue":{"value":{"entity-type":"item","numeric-id":5713510,"id":"Q5713510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f07824545af51374baaadf39e77c4e4783d4d4a","datavalue":{"value":{"amount":"+0.88700116","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":"Q888467$C5820767-139F-4A3A-A5B0-64C2C76BBD8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb253fb55714f511287e3fb7db3bf54cfc2f7066","datavalue":{"value":{"entity-type":"item","numeric-id":5311270,"id":"Q5311270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f07824545af51374baaadf39e77c4e4783d4d4a","datavalue":{"value":{"amount":"+0.88700116","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":"Q888467$B1E17511-89D8-48F8-890B-17E3192D2C09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfec26b6ca7d4c46b8a259ec92a2c7b029833656","datavalue":{"value":{"entity-type":"item","numeric-id":4930589,"id":"Q4930589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bc4029065d30d2129c092ea53086aa3dee0a52f","datavalue":{"value":{"amount":"+0.87212896","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":"Q888467$B25003F1-3D18-4BBF-B2ED-C807ACDD165E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9f170836a89b0e3c095f5750023447b1c93aa81","datavalue":{"value":{"entity-type":"item","numeric-id":5326331,"id":"Q5326331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e486ab8134c35bae989ba01d27bb806c8dfe898a","datavalue":{"value":{"amount":"+0.8711677","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":"Q888467$D94CA931-8A6C-4DC2-AC2A-49ECF85EE024","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e2f42da8edbca079b6a499d2bad177c9e5e69247","datavalue":{"value":{"entity-type":"item","numeric-id":6102162,"id":"Q6102162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1fc127a5f558ac5a5f2c39142c2b093906e4c628","datavalue":{"value":{"amount":"+0.8691517","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":"Q888467$40C1DB6E-507A-40A4-A15B-DE3D67F7CB43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"992fa52f09fbfce42db0c1f9839dc4ce41532293","datavalue":{"value":{"entity-type":"item","numeric-id":5458343,"id":"Q5458343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"608b0f15aab75d88e187c362ed14cf6d38937ad3","datavalue":{"value":{"amount":"+0.86560214","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":"Q888467$BBB5EC4F-574B-47B7-B122-90C13F882B9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f4f48a2b7882d03de41a9fb8d6f1df3fcfcde538","datavalue":{"value":{"entity-type":"item","numeric-id":4942016,"id":"Q4942016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd84ff425391ecde76a6eb7674051f3807e87eac","datavalue":{"value":{"amount":"+0.8647928","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":"Q888467$E0DEF8BB-C78C-4A1E-A1F8-5F896763B7C4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Optimization techniques for Craig interpolant compaction in unbounded model checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Optimization_techniques_for_Craig_interpolant_compaction_in_unbounded_model_checking"}}}}}