{"entities":{"Q253964":{"pageid":255731,"ns":120,"title":"Item:Q253964","lastrevid":60347628,"modified":"2026-04-10T16:36:11Z","type":"item","id":"Q253964","labels":{"en":{"language":"en","value":"Solving QBF with counterexample guided refinement"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6551548"}},"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":"Q253964$5708BCD3-F63B-4282-B378-44CFF6190CEC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b014e54caa7fc301f23086a20c20b2ed189157b5","datavalue":{"value":{"text":"Solving QBF with counterexample guided refinement","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q253964$956BDF9F-8BD9-481D-85E5-98AF641AC46A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"36db6869f13f7ae040c94ee711adb9cd0da33941","datavalue":{"value":"1351.68254","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q253964$743CAAC8-4FB4-4309-8321-D798BF6B6521","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e24c4e43654848209a68060f96d6b8df113db0e5","datavalue":{"value":{"entity-type":"item","numeric-id":253961,"id":"Q253961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$A047C88A-2F84-4547-B0EC-F8BBB0C05F41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"822a078c7a4829031fff924b3165e7b6eb2f1e2e","datavalue":{"value":{"entity-type":"item","numeric-id":253962,"id":"Q253962"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$DC9D3C65-6808-4CE3-8B65-0CA720C0B9E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"41df06f4fe4133fafd7ede4eda94dd022be9bb8e","datavalue":{"value":{"entity-type":"item","numeric-id":1430295,"id":"Q1430295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$9B2D1E1A-AF77-4E2D-B2D5-78EF96189676","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4e4e5ed72bee66087d415d4f69d49eefd101a453","datavalue":{"value":{"entity-type":"item","numeric-id":526749,"id":"Q526749"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$2ACC9670-73ED-48F0-BB83-735CABB64D05","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"984e6510ec40a363d20e607cce2cc2f8b07918ae","datavalue":{"value":{"entity-type":"item","numeric-id":72340,"id":"Q72340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$6640C2ED-9330-4B81-AAFF-3EB78284DA13","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0d64657497f836ca9759a26855d3a3e0d86319c6","datavalue":{"value":{"time":"+2016-03-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q253964$91D6E5D3-3AA3-4EC9-B9E1-D55D1800C20E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q253964$903BD148-DC66-4516-96C2-8307E70555EE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a286a18dfe735ebdfc22876e4f4b4c89a1212754","datavalue":{"value":"6551548","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q253964$46EB7DB9-4EB4-4792-AC5C-9C175C8B6677","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4dc78b1e4558056e875de92cbf8329d0562afe86","datavalue":{"value":"QBF","type":"string"},"datatype":"string"},"type":"statement","id":"Q253964$ABA84BDE-BCF3-4022-862D-A80F0FE41A01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a56e5793ea33870a204239ad40fe7f02bf24fac2","datavalue":{"value":"expansion","type":"string"},"datatype":"string"},"type":"statement","id":"Q253964$A84D54C0-D70E-451D-B059-B80DE08E6211","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"319f0259a406af2d877e55e6b98156b841ef9913","datavalue":{"value":"counterexample guided abstraction refinement (CEGAR)","type":"string"},"datatype":"string"},"type":"statement","id":"Q253964$6E712CA2-C085-4C2F-BA20-A336E1FCA38D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9f9aebdd1b3f62380f4707b4956c9497d9985521","datavalue":{"value":{"entity-type":"item","numeric-id":55702,"id":"Q55702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$0E0E80AE-DFA7-4BA3-B590-3DCF766498D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90bbf05b61d9b805bad3a7dddfdf703eeaec6239","datavalue":{"value":{"entity-type":"item","numeric-id":19022,"id":"Q19022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$8E77E9A2-5CF6-4459-B002-0E2C73AF8935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1ef66678d684041b8de78c7576de4cf0ad3466f3","datavalue":{"value":{"entity-type":"item","numeric-id":21560,"id":"Q21560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$5E0AE0BF-C96E-4909-B31A-86529517DE8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"51a313bba85d083d332055ca3bb709d116ecc30a","datavalue":{"value":{"entity-type":"item","numeric-id":21559,"id":"Q21559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$58EEE9CC-BBAB-49E5-9DA1-F0D19199DD0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"87973a7a71e3ffa05ce5b5aeabcd6b005b85607e","datavalue":{"value":{"entity-type":"item","numeric-id":21561,"id":"Q21561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$87974CF8-C3F7-4572-BF0F-5CCDDDCB6646","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b80a8312448a75ce18cad949570147edd296704e","datavalue":{"value":{"entity-type":"item","numeric-id":40097,"id":"Q40097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$ACFCC050-83E3-4516-B50D-D4687721A9F7","rank":"normal"},{"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":"Q253964$D8827048-06DB-4037-A003-93F66C49E266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8cc02a4d5cfe357c7398b8045c9b55b5580560aa","datavalue":{"value":{"entity-type":"item","numeric-id":19323,"id":"Q19323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$AA0E2D7A-2FEC-4008-B73F-F5C0A7DA2CDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a6b38d41f42be9a63abc418d73603b2d531b26a9","datavalue":{"value":{"entity-type":"item","numeric-id":21713,"id":"Q21713"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$62A2795A-F4F5-45F8-BE14-3ED503D42FA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$7B55B68E-8BCA-4094-BE40-932F24F4A442","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6ef83bc65a4e27e40a0f15cc6aef8f4086b5991a","datavalue":{"value":{"entity-type":"item","numeric-id":23327,"id":"Q23327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$1B282B05-118B-4647-9C43-DF5BDCCEA2B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2c9183463f88b5847f6cb1fa629a2f0b9ed00778","datavalue":{"value":{"entity-type":"item","numeric-id":23326,"id":"Q23326"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$588CDF24-B554-4845-B3C6-1A9EAB889545","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":"Q253964$323C8C09-03B5-45F3-A98B-51508EA9CE87","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0eea586824817aecd83009cb10c64acd51a86afa","datavalue":{"value":"https://doi.org/10.1016/j.artint.2016.01.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q253964$E3B93C7D-5E79-497D-91DA-3AFB135DF621","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ec3733d4f95fd6a184d7a9f10d7d109b71aebbe6","datavalue":{"value":"W2233304325","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q253964$FBEF7D17-955B-4FF5-AEEA-14D411A45F43","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"c346dfbbaaed5d94a1c01c4c73e55ae8d0515baf","datavalue":{"value":"Q62047276","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q253964$4554A42A-BF17-4380-918D-0ECBD319FABB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ebd47a55b9c2aed7b10858aad59c96098e81642","datavalue":{"value":{"entity-type":"item","numeric-id":3620436,"id":"Q3620436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$849A46E8-3284-453F-B699-35EB9F5DCFDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25a650df3daffe41a5463985884e68be23fb4743","datavalue":{"value":{"entity-type":"item","numeric-id":5705931,"id":"Q5705931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$171AF8B2-86FC-4812-9C87-27CB6D062B36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a27d1fb90cccb11f35259877f3ba9e207a2057f","datavalue":{"value":{"entity-type":"item","numeric-id":3502708,"id":"Q3502708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$27EAB39A-A993-429B-8BB7-31275836D263","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fda6711bd23a75752359e8da91eea58b1ea8ddac","datavalue":{"value":{"entity-type":"item","numeric-id":3612470,"id":"Q3612470"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$A6F030B9-9A3C-49CC-8E56-7761BC48DB58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4329c832aaeefb18d7073f9e13d9d92559128df4","datavalue":{"value":{"entity-type":"item","numeric-id":4930581,"id":"Q4930581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$606F19CC-534A-48D8-B78D-AB9C08E25A0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f74ab2dd5044d6998656533da5ea01adebaf165","datavalue":{"value":{"entity-type":"item","numeric-id":3007688,"id":"Q3007688"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$11534B9D-D769-4F0C-AA68-1968DE6CEC40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ebdb78748228ac4fd7f7ad8a904ebbfa617c0fe8","datavalue":{"value":{"entity-type":"item","numeric-id":5756571,"id":"Q5756571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$F2B47884-879C-4561-B1B9-4473EBC917EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"926ec579a6e1751bee4f751c2a20e927df8e0825","datavalue":{"value":{"entity-type":"item","numeric-id":5200018,"id":"Q5200018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$3A1FF374-C42B-4D3F-9D9D-D0AF6D454888","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad5843107a675ef426cb1b75becf5e9aa46b5362","datavalue":{"value":{"entity-type":"item","numeric-id":5900311,"id":"Q5900311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$2ACB3678-687D-4977-9A5F-D974AD7CBF4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"543029396b2329940995625ede0271d1756b19bb","datavalue":{"value":{"entity-type":"item","numeric-id":5394625,"id":"Q5394625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$DC900CA5-5139-4761-B7C2-92517D8A61D1","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":"Q253964$A31B14B6-570D-4D88-953A-FF6261348C8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b6b8ac53c9c616c3aedcca87f608c4737d5fa97","datavalue":{"value":{"entity-type":"item","numeric-id":4412858,"id":"Q4412858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$0F8B0670-0B73-4CE6-A29D-DDE813D63370","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":"Q253964$CF8F5F94-018E-4F28-89E5-D7970C53C4EC","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":"Q253964$258D49B0-5C54-45FC-8539-AFC983C83FBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c6b871d25a3f2bcc10ef5d12d2a6df59054c7c5","datavalue":{"value":{"entity-type":"item","numeric-id":5604434,"id":"Q5604434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$85B1EE38-2B09-44B8-9518-AD404893A69A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"008723b33cb14bbda59226503d753d137dc6f8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1098330,"id":"Q1098330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$7DBF16E0-331F-4AEE-989E-726EF96FC544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3479b1b8ce1eb8a8699c52a172d26d4d947366b0","datavalue":{"value":{"entity-type":"item","numeric-id":4298260,"id":"Q4298260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$13B9248E-9E7D-4522-940B-46DE45EAA61F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72df03d77e1bc06662d09c4718408a862df26da2","datavalue":{"value":{"entity-type":"item","numeric-id":1891159,"id":"Q1891159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$82F4428C-A398-4D62-8E2F-1B327FD74392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e5a439ad8d4c6ab1137e52e48a534b00e2b2873","datavalue":{"value":{"entity-type":"item","numeric-id":606909,"id":"Q606909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$BADF96B8-A582-40AF-B2F7-C934C0CCAA4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6da6ded218db8e1aba2fc38982f0c41333c8292d","datavalue":{"value":{"entity-type":"item","numeric-id":4809077,"id":"Q4809077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$AA16204E-CFA8-45CA-9BB2-6D6A7D464A2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dc64d6d31493ac74da4f6c177f509ec4a9d4b14","datavalue":{"value":{"entity-type":"item","numeric-id":4804899,"id":"Q4804899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$FA53FE0B-6E6D-4F37-996E-ADA35C48FCDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d606ca29a316c6d13ac236e9ee6da4bfadd6eb91","datavalue":{"value":{"entity-type":"item","numeric-id":1604210,"id":"Q1604210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$248241DD-FC79-47D7-9175-425F37F066CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc8e7aa6809d54e2ccf2352967b475ad93db72d0","datavalue":{"value":{"entity-type":"item","numeric-id":4930584,"id":"Q4930584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$3D892EB1-45E7-4C5E-9E46-930535CA4E0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55b1c8183df1009d3675586de65e7dfd8c2c37ca","datavalue":{"value":{"entity-type":"item","numeric-id":286397,"id":"Q286397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$7B2D4A1B-BF19-4DE3-A8C4-59EDE58884DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dedc1a1dc66375148bfb7c52438affa8128f4c1d","datavalue":{"value":{"entity-type":"item","numeric-id":4930601,"id":"Q4930601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$E24AA030-8A8C-46E2-9FFF-A21F6A2C7FBF","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":"Q253964$922BC503-5EC9-4E5C-BB33-A3E55C0D7042","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8e9c7dfe2263cb88548446838aa8cb493a7f9e1","datavalue":{"value":{"entity-type":"item","numeric-id":5325879,"id":"Q5325879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$6A235520-094F-45BA-81CF-1CC30E103F7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2a66a16d4f6036909c76a0ad366001db31dea77","datavalue":{"value":{"entity-type":"item","numeric-id":4930765,"id":"Q4930765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$AB995AC3-13AB-4D77-9E9E-FCE4CD931BF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19c0f6e16691d3be7f09aeb1f46536b8cc5b9c84","datavalue":{"value":{"entity-type":"item","numeric-id":3524206,"id":"Q3524206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$CFEC9A1E-CACC-470D-A584-8840EDC1FF66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adb2002aedbf2ef2b94f7cf9ba9a2a7aef436cd5","datavalue":{"value":{"entity-type":"item","numeric-id":3566747,"id":"Q3566747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$A8FA70E8-4309-416B-9D06-CD24C030CD1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77025c29d5290494072647e90cfd5b7ac95c54f8","datavalue":{"value":{"entity-type":"item","numeric-id":4427904,"id":"Q4427904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$1E3370F3-EEAF-430E-B696-D7A6A59A64CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f7f7b41cbf8e7677b95d005680bc21b9f8ae86d","datavalue":{"value":{"entity-type":"item","numeric-id":5326462,"id":"Q5326462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$2EF2609B-6362-4159-B7FC-EEFB3EB3ACDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"120ccad2cdca56cef7c6cf55185b9724569b94d3","datavalue":{"value":{"entity-type":"item","numeric-id":5326468,"id":"Q5326468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$26870016-1BDF-4C01-A98C-C1112AC41F42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71c88d50fafd6c2eb4794d29690488c214748da9","datavalue":{"value":{"entity-type":"item","numeric-id":5326454,"id":"Q5326454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$5861E3AD-CADB-41C9-83B5-1DD5730B57A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04c9dc9e7a7e7ba60691fd7bebd8fdd9e32563f8","datavalue":{"value":{"entity-type":"item","numeric-id":2922598,"id":"Q2922598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$91BEB3B9-CB97-4C77-A662-ED2E6F08452D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d4ba72b99f6b7c8f1619ec42b1fca7ba63faae2","datavalue":{"value":{"entity-type":"item","numeric-id":4899301,"id":"Q4899301"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$29D733F2-E127-401D-9350-C1EC7956132A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"024f5f642d34b86085d7b9145b61316e312fd268","datavalue":{"value":{"entity-type":"item","numeric-id":2441712,"id":"Q2441712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$6DE91633-110C-497B-897B-BD299E515729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46a64f5d8bb8796d929b170b9a451b694680664c","datavalue":{"value":{"entity-type":"item","numeric-id":2339467,"id":"Q2339467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$DBCD5149-8146-42FA-9EE5-CABB72FA23AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85c9f74c9e2f323d6a6a8fb50accb2001547c77d","datavalue":{"value":{"entity-type":"item","numeric-id":2954985,"id":"Q2954985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q253964$0ED86C9E-6278-4CD3-89B4-933A942A5B93","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":"Q253964$4D9218BD-EBE4-4C59-A5EF-53CCCB075A72","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4c36472091441d176397469d95f49d8aa462db74","datavalue":{"value":"10.1016/J.ARTINT.2016.01.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q253964$B83B6383-AF55-4200-9136-E43024B571E8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44fd65f52ee036a7c3846fcf7643553a6b9cd9ff","datavalue":{"value":{"entity-type":"item","numeric-id":2843327,"id":"Q2843327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a5b05bab1e28815a239856b2198f2f4aab8526b","datavalue":{"value":{"amount":"+0.8935925364494324","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":"Q253964$CDF2B99E-96E0-413D-BC97-2D2BB2FCB423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddd56edf54f27508795f985fdb8fe850a23e1491","datavalue":{"value":{"entity-type":"item","numeric-id":2164249,"id":"Q2164249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c59b91e5f28c7522fbd2cc9d0c3bc7ae55d23e5","datavalue":{"value":{"amount":"+0.8217137455940247","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":"Q253964$AF85850B-98CD-45CE-BF96-81BBF8AED202","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e90393cb1a4862c6b22503feae877e5b45f2365","datavalue":{"value":{"entity-type":"item","numeric-id":3007686,"id":"Q3007686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82a699b9fdc26523cf02d35c4937a3e598436f7c","datavalue":{"value":{"amount":"+0.7712345123291016","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":"Q253964$BAD995FC-ADEA-4550-9A79-2B53A2933678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e3fa43ea9a72a83663cc0ab045250bfd2bb9f05","datavalue":{"value":{"entity-type":"item","numeric-id":3460072,"id":"Q3460072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d335794442e486b9ff557f0ec08e8bb168ec5061","datavalue":{"value":{"amount":"+0.7653603553771973","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":"Q253964$F7BFD70D-049E-4460-A586-C4912C735B0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"741673679e1460f40e1a8b02e221f185fbfaa111","datavalue":{"value":{"entity-type":"item","numeric-id":3637177,"id":"Q3637177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ec2db1c0a3c423fe268f7a01c48720463e4d7f1","datavalue":{"value":{"amount":"+0.7462427616119385","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":"Q253964$B92D52B7-63E5-4C02-B1AD-F1BC501311DA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Solving QBF with counterexample guided refinement","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Solving_QBF_with_counterexample_guided_refinement"}}}}}