{"entities":{"Q7034849":{"pageid":21711978,"ns":120,"title":"Item:Q7034849","lastrevid":77522588,"modified":"2026-05-04T15:32:40Z","type":"item","id":"Q7034849","labels":{"en":{"language":"en","value":"Fast and verified UNSAT certificate checking"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7977168"}},"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":"Q7034849$48F07241-8CB7-4284-84A7-A7B9388882EF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1278db406fa17d21ba7adacbdc48d03840409827","datavalue":{"value":{"text":"Fast and verified UNSAT certificate checking","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7034849$BA0FBCEE-A543-4F49-86CC-7D4ECCC66472","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7c417cd21747371825b53819658fdebc7167028f","datavalue":{"value":"10.1007/978-3-031-63498-7_26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7034849$BD24D732-7DED-40B0-A593-A2AF1998436C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8e4be225a6094490d6530fbb2f56929f5bbbcf0","datavalue":{"value":{"entity-type":"item","numeric-id":682349,"id":"Q682349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$E9A7F5B6-B1B7-4E9C-A215-D2600469A6D5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"faebccf51ad7ddcce1eed4a97c7e0eb92d585316","datavalue":{"value":{"time":"+2025-01-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7034849$E2F6C52D-7FC4-401D-8B31-614F71B92C13","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7034849$B713E494-1966-4C62-BC18-BC32A594DB65","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8b97d738ce888270bfa288803e216b92c8956059","datavalue":{"value":"7977168","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7034849$52C5D543-BC87-49C3-A2BA-B08F25662783","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":"Q7034849$257A2E85-ECCD-4CC4-80B8-8511187C6B09","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c75618434d73fdee40b3df44c518010e9b89579e","datavalue":{"value":"UNSAT certificates","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034849$01A61283-EB99-4932-8F96-2C7EC06B513D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"914c4fb672c5e9fcb02ce3cac02eea7131783a06","datavalue":{"value":"LRAT","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034849$E8E7BD5D-9D25-4765-81CC-6F8490226E0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85aed4699d6b444cae1cfc69ed972cadec2ca21f","datavalue":{"value":"Isabelle-LLVM","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034849$9BCD3DE6-DD2C-4AF6-B134-B962B372CCC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d784eec07510825c8d9b075d048bc26b86cacfe5","datavalue":{"value":"verified software","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034849$460A8B99-1CFA-417C-8620-4E168A7738E7","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":"Q7034849$F6421C0D-C438-4589-A2E7-BCCB8B9E4905","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"21bc7f5722febfc46378708c5308d47dc3e9fd15","datavalue":{"value":{"entity-type":"item","numeric-id":2044190,"id":"Q2044190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$5A408223-39E8-4648-993C-BFC256B22DD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c93b9148de1ac8feaebf7881241c315fd260b962","datavalue":{"value":{"entity-type":"item","numeric-id":6488808,"id":"Q6488808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$15F4B89F-575E-48EE-9D8B-5315A38A6B13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5ccea7b6fe9f5a7082344f9edaface083da76","datavalue":{"value":{"entity-type":"item","numeric-id":2405252,"id":"Q2405252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$784D6360-8ADA-4689-8A66-935FD2CB9BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d43182de98d159f0ebb543c5126e0ae385036ba","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$C3EE3FE8-252A-4585-A2F0-1C6409A8899D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2d2cf5aa71dbe166cb74aacecac561d9e3d134b","datavalue":{"value":{"entity-type":"item","numeric-id":2892741,"id":"Q2892741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$049E831A-037E-401B-911E-468BE9018C89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e153234bedc671890e46d97b503b862efeb995a","datavalue":{"value":{"entity-type":"item","numeric-id":3558235,"id":"Q3558235"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$953DCF1D-3B84-44CF-ADD1-353A6128A867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5dffe5441220fd05c9ab29a095f510d384d606b","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$DF1A8ECF-33DD-45F1-853D-73A091DCA121","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77bf0527cae45caf1270972ff5ead3c89685a7ab","datavalue":{"value":{"entity-type":"item","numeric-id":5875431,"id":"Q5875431"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$4D0FF603-E359-4312-82C3-2C219ED4133C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1951f16d4fe8a611f755a4887c35002e0149e28","datavalue":{"value":{"entity-type":"item","numeric-id":5919480,"id":"Q5919480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$C20CDAA3-B5FD-4C5B-88C4-2D9D7362F9BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7f766bae7bb1dc745731294a8b2405f79150a41","datavalue":{"value":{"entity-type":"item","numeric-id":2914741,"id":"Q2914741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$0E0C908A-1D03-4441-BA99-140B75516E64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cce922860f2a1126d5854cee853b0a72b2ecf9c3","datavalue":{"value":{"entity-type":"item","numeric-id":6643101,"id":"Q6643101"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$7759BA9B-4890-45FD-86D7-D244672B290B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e99741ea86af8e3fe4690d90c224835231a7ef4d","datavalue":{"value":{"entity-type":"item","numeric-id":2233509,"id":"Q2233509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$1307EC04-319E-44FE-B4BA-3E6DDA38AA36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb081c24d3f308759ffc5be25d93bb06a52b464f","datavalue":{"value":{"entity-type":"item","numeric-id":3192088,"id":"Q3192088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034849$17F9556D-E3AB-4F68-B5F3-EFE734345038","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Fast and verified UNSAT certificate checking","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Fast_and_verified_UNSAT_certificate_checking"}}}}}