{"entities":{"Q2181940":{"pageid":2192683,"ns":120,"title":"Item:Q2181940","lastrevid":57763338,"modified":"2026-04-02T10:32:05Z","type":"item","id":"Q2181940","labels":{"en":{"language":"en","value":"DRAT-based bit-vector proofs in CVC4"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7202464"}},"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":"Q2181940$A78229E8-9E91-4DF7-B397-33B36AB8558A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0c62fc07ee626a5cedec9949d6263c8e6d776a68","datavalue":{"value":{"text":"DRAT-based bit-vector proofs in CVC4","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2181940$AB0DE2F6-D4E6-4A5B-9A7D-6E30415364DF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"12abfb4a4064cc6e97f7dd834f5b5ad676be1fa5","datavalue":{"value":"1441.68235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2181940$3A8F917F-F70F-4153-ABC1-82B78866BB3A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"81cdea18abc480513ee14f500f8dc33d08b8873d","datavalue":{"value":"10.1007/978-3-030-24258-9_21","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2181940$854F9EBC-47B3-429F-AA56-773CE86D4312","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"474e6105f02e45fefcee26c442791da046a2f700","datavalue":{"value":{"entity-type":"item","numeric-id":2104493,"id":"Q2104493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$21A173F0-B9A1-46FD-8220-F591EE941559","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d1797629fcd98376075f8fdfe9a9fcaf30af9290","datavalue":{"value":{"entity-type":"item","numeric-id":1688544,"id":"Q1688544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$0BA39F88-A613-482B-8B64-5E64E0A3608F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8675088ba59622264d9b63deab589caaa3c7b74e","datavalue":{"value":{"entity-type":"item","numeric-id":1688545,"id":"Q1688545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$8532BA28-3315-45DC-AE2F-EDF5575B4CD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"15c3e77937a4117931d77ceeaa33fe1a7a5d9cf0","datavalue":{"value":{"entity-type":"item","numeric-id":1682295,"id":"Q1682295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$63EB614A-ABBE-477C-9D23-42F2B1801998","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":"Q2181940$E1458DEB-6690-4FE2-8B8D-DF118A8B52F9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8d777a513c8a436f6b680a1e02c588f4cd3d39d0","datavalue":{"value":{"time":"+2020-05-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2181940$CB37EEAE-997E-4093-BBB9-15AE53C24A2D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5425492b159a2b860673ce37646fb983a0045862","datavalue":{"value":"https://arxiv.org/abs/1907.00087","type":"string"},"datatype":"url"},"type":"statement","id":"Q2181940$FD6EFA06-2983-462D-8DFC-6BB55841AD7E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2181940$AF241B22-57C7-4DEE-AA2A-0ECFAB2471AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2181940$0E7B9090-6479-4C08-BC98-AF7B2C783AD4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2a3a3aecdceb29b22baf5169568e248fd0338b76","datavalue":{"value":"7202464","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2181940$CAEE03FD-BB7F-48E7-A062-93B1DFC393A8","rank":"normal"}],"P1463":[{"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":"Q2181940$03D4F7B7-7955-4C0F-A8DD-AEA492529D1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3b163eb2acfaa09d2ebf57c54881fcc37ef41973","datavalue":{"value":{"entity-type":"item","numeric-id":22051,"id":"Q22051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$330D1782-3A96-4CEF-9856-11FC8917F240","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a3f7f8548c5af1e2ae512d0bcfba5384da7ef3bf","datavalue":{"value":{"entity-type":"item","numeric-id":25228,"id":"Q25228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$FEFA0F27-5E0B-47FB-8BFB-DB0FB288E290","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":"Q2181940$4509851B-0364-4E31-87B8-8C7FE5F91DA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f29f161a221c0bedeec97e9d4ad10664227f4777","datavalue":{"value":{"entity-type":"item","numeric-id":16290,"id":"Q16290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$40112831-2278-4BA4-98F1-35DF528C3C16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$EEBBDB95-0F90-4EBF-A986-F271007F5E11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5b9460a01ea60cde385cddccbe3b63d66f761f84","datavalue":{"value":{"entity-type":"item","numeric-id":44021,"id":"Q44021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2181940$97562AB3-2B64-4C2C-A5DD-3B2E16A5F0D7","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":"Q2181940$E4AFC837-A640-4A76-947F-A54ACFA04933","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6c958d123e68b9e4aae3584b658159fc89325549","datavalue":{"value":"W2963523951","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2181940$4F28670B-6A6E-4A14-8EFC-0F04D59A7F0E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"206e03f025f2824888a45535e703fd7faf344800","datavalue":{"value":{"entity-type":"item","numeric-id":4502480,"id":"Q4502480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2463f05a39cab94d66ab3bb57317abb89ebed04","datavalue":{"value":{"amount":"+0.8251973","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":"Q2181940$0655BC03-0DD4-4B8B-8780-FC21E51DA99E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4bc2b378fb2f30b12aefcc50a9172be3f805169b","datavalue":{"value":{"entity-type":"item","numeric-id":3058755,"id":"Q3058755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53e56c4a52d4cbd5be8e01a59d31eb88715b98f9","datavalue":{"value":{"amount":"+0.82487774","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":"Q2181940$01701F9F-C2C2-4090-8E23-9BC8993CDCC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c0d075bc423b267dce1964b6e694f03b4ace44d","datavalue":{"value":{"entity-type":"item","numeric-id":2807226,"id":"Q2807226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b0a269d8ca63def49a69e267661d39a403dd05b","datavalue":{"value":{"amount":"+0.81800133","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":"Q2181940$2877618F-2BD9-4647-B5D6-DC08419B052D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cea9292e19a28b40c83958a96951b373440b326","datavalue":{"value":{"entity-type":"item","numeric-id":1648779,"id":"Q1648779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df233e5acb75a1871362df07af5927a98a56d40d","datavalue":{"value":{"amount":"+0.8175219","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":"Q2181940$786B0A69-FFF0-4CEA-AC5A-1138CE1EF3BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"754371e75e790d6f6f3c20a97a5ffe4da61db280","datavalue":{"value":{"entity-type":"item","numeric-id":1749613,"id":"Q1749613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa4a2b359603c96729635f5fa20e68e626cf5d96","datavalue":{"value":{"amount":"+0.8162704","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":"Q2181940$8B238F98-128F-4452-81B2-B1FB0A350523","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cd126aa1fad76afa618bf17dcdbfe9aff67826f1","datavalue":{"value":{"entity-type":"item","numeric-id":1641169,"id":"Q1641169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07d27cf6efdf00f443a4182c498f152221af5752","datavalue":{"value":{"amount":"+0.81555545","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":"Q2181940$06F84C55-AF4E-4572-86F9-DFB0EE1963CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38ca69dbb2a24d3517677fc5d81e39fc165e7937","datavalue":{"value":{"entity-type":"item","numeric-id":2181921,"id":"Q2181921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"00d0370f53ab2a9f2815a734bfc68eadc9b9d118","datavalue":{"value":{"amount":"+0.8136851","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":"Q2181940$2F1E1B3C-93A8-489F-8285-6527291C63B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"60044ccd7560f93e36e6159d039cd5f4217f14ec","datavalue":{"value":{"entity-type":"item","numeric-id":5422484,"id":"Q5422484"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3da4649390587f9fd43af53133d8ccf98774c977","datavalue":{"value":{"amount":"+0.81247056","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":"Q2181940$CE1C18B9-8608-4B81-866D-5A9747481B7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16791845f07ed63418c9d6ce62b4b8e0c3673346","datavalue":{"value":{"entity-type":"item","numeric-id":1799250,"id":"Q1799250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32abd639c0effff175f997dd043b9456ea1fd0ae","datavalue":{"value":{"amount":"+0.8106801","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":"Q2181940$B29FFBAA-7336-4C02-B76B-B361B48ED0BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bddc75bd5283755a39fd226c4731b422f6cc5cb4","datavalue":{"value":{"entity-type":"item","numeric-id":5428115,"id":"Q5428115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7be272db1546bd0ef6cffa489a0e25070ca4529","datavalue":{"value":{"amount":"+0.8097423","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":"Q2181940$4533EFE1-D9F1-4CAD-890D-D61572931980","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2181940","badges":[]}}}}}