{"entities":{"Q1006728":{"pageid":1008576,"ns":120,"title":"Item:Q1006728","lastrevid":66566616,"modified":"2026-04-12T10:59:30Z","type":"item","id":"Q1006728","labels":{"en":{"language":"en","value":"Integrating external deduction tools with ACL2"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5532933"}},"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":"Q1006728$EE494A1A-7ED0-4131-81FC-DEEC32C25FBC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"567b99c4a811b908f205e23fdf96c624386c0bf9","datavalue":{"value":{"text":"Integrating external deduction tools with ACL2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1006728$D6A3AEF5-9B6F-495C-A6F4-3902004F9AB6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2efb2ae1c2c52e75b0488ef26e1d28b16a67f9f3","datavalue":{"value":"1183.68558","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006728$977BFD49-06A6-4DDA-AE49-9D65AEE9483E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6bbab2ea230ef82cf7d72bee404dd827d5aaeed","datavalue":{"value":{"entity-type":"item","numeric-id":230814,"id":"Q230814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$BC609A18-FA37-487A-836E-CEFAE8562BDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f5a9bcb5f8b5c271cc4d9ccff897b2db1a111ede","datavalue":{"value":{"entity-type":"item","numeric-id":540689,"id":"Q540689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$E4883033-2F1B-4900-8204-E8E0F21B5373","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1174786862e71116099c6ebb313b0b584e6ff3d2","datavalue":{"value":{"entity-type":"item","numeric-id":1006727,"id":"Q1006727"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$79FC3573-C548-45CB-9534-29AFF6F6D29A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0d384413a2d1b8185eb46b74e5b2c74244e0aac","datavalue":{"value":{"entity-type":"item","numeric-id":928667,"id":"Q928667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$1F69570A-2993-4724-B26C-23FEEB69C1A9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fd9c858b64e538228c66f00c768fd1506ee71010","datavalue":{"value":{"entity-type":"item","numeric-id":124852,"id":"Q124852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$25DC2E44-2180-40C6-812A-9AFCF93D868D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f17d548f42efb27321ed2d9ca45a732b10fcb2c","datavalue":{"value":{"time":"+2009-03-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1006728$2B121E4F-3188-47E4-BCCC-4545D6048AAE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006728$1E0B02CA-DEBC-4501-9D1D-2425E425D126","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006728$C18AF43B-1356-4236-BC36-1F22D97EEE83","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"62fff1bbfd37544b232e04c3d5a1e18334951770","datavalue":{"value":"5532933","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006728$F1F5593C-AF0D-4189-A1E8-C136C5DD6124","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1ca1042868ff4f694776e4b2c62ec66638c4ef91","datavalue":{"value":"automated reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006728$443B0B29-38F8-4F75-BF2F-CCE8050EB54B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006728$28BE6DAE-4D8D-406B-B746-0832CCB9EA56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e2e80a7123e4ea6d0418cb24d37b1837f13e3514","datavalue":{"value":"first-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006728$8F87304F-0EA1-4A04-B22A-D7A2657CF9E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f80d68e3c12b442d5c3fd8c97262c92d38404795","datavalue":{"value":"interfaces","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006728$A91947AD-9E12-42DC-B5A0-DD73620CE543","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1006728$B5A87B1E-E792-4D2A-B13D-1EE845366ED9","rank":"normal"}],"P1463":[{"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":"Q1006728$BE4E81C3-E1DB-4494-A106-AC7E8F7218CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8f057223c758d6b8295ecbdef4842faac2ccb72","datavalue":{"value":{"entity-type":"item","numeric-id":19253,"id":"Q19253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$F6A85A12-7E23-4A66-9135-BEDD0FCCB572","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"233bd03fc74bc4c01e6f828569e5eb13f94bb747","datavalue":{"value":{"entity-type":"item","numeric-id":22242,"id":"Q22242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$F75EA397-1AD2-49C5-BEEB-69A65F63AA83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b48d7b42095141e48a9c1788caedf5498122de8b","datavalue":{"value":{"entity-type":"item","numeric-id":31441,"id":"Q31441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$A68BC8A6-7385-4B48-B818-63CC81743765","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$417B5D22-6CD8-435B-9553-829B54FD9784","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":"Q1006728$D563479E-4255-46C5-A337-C4272917CF4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"76802187a7905926b2a38ec174758f899e34b9bc","datavalue":{"value":{"entity-type":"item","numeric-id":22347,"id":"Q22347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$DCA524F5-6FE1-4C5A-B4E6-256F530F912D","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":"Q1006728$6E424187-5644-4465-A9E9-55FA93A314AF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"63c08442de147947cb5ed3dd7872145df0a883f4","datavalue":{"value":"https://doi.org/10.1016/j.jal.2007.07.002","type":"string"},"datatype":"url"},"type":"statement","id":"Q1006728$423B8C8C-1129-44BB-BD7B-24C810EC6C51","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d0da374da0af9933266f9a8fd12c602ca5fe34c5","datavalue":{"value":"W2024791001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006728$AEBEE077-EFE6-4AC2-8EC4-CB416B0CB162","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5019b1606a46a3d06c91c12c8fdfd5e1609d2542","datavalue":{"value":{"entity-type":"item","numeric-id":1006728,"id":"Q1006728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$C8852C0A-D8D2-4488-858C-2CE5ADF6B434","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe3b950411ee1e7918837695edeb889a33306058","datavalue":{"value":{"entity-type":"item","numeric-id":5452599,"id":"Q5452599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$BD9079D9-CAC6-42E1-8C5A-9F88A49BF308","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f72f65644d666e389907b7173225cdf0065502fd","datavalue":{"value":{"entity-type":"item","numeric-id":4571480,"id":"Q4571480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$1B7D8035-92FB-44E0-8C17-8C31F3C3A0A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afefbaf137f83b64b00e4ef48cc98682850f21d5","datavalue":{"value":{"entity-type":"item","numeric-id":4230664,"id":"Q4230664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$07205FF1-62FE-41FE-A875-5AD2D50F4037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca6926d9a2864657c63c8ba6d81f03198b036942","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$D136369B-CD43-481E-9D5A-6421EF433203","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bce4f5ae886a6add198cde1454a758dfcc3c40fe","datavalue":{"value":{"entity-type":"item","numeric-id":3932277,"id":"Q3932277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$5DF96214-5F66-4471-9978-4F7D225DE294","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9635365b0780328d7ae22bc69b462e7144999d03","datavalue":{"value":{"entity-type":"item","numeric-id":5573961,"id":"Q5573961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$1D331FB5-A6C8-46C7-9130-9AFFB3E21D36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01cc0603799551d88cdcf60c08da4c96b4eb1c0","datavalue":{"value":{"entity-type":"item","numeric-id":5900722,"id":"Q5900722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$08FA03EB-F1C6-4316-87B7-BFEA4A6F44FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"283b457c1aa928df8cba388628638010a8a9e043","datavalue":{"value":{"entity-type":"item","numeric-id":4016540,"id":"Q4016540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$4D783C2B-23F1-4264-9D00-AB72F439BC18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca3010d203b6bfbb9b241f39c49c210f8a2b5dee","datavalue":{"value":{"entity-type":"item","numeric-id":5492967,"id":"Q5492967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$E1471F4D-2795-47A1-8BB5-8727FB37D85C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80015c982f395703eb961f7d88d9ea85973eed1d","datavalue":{"value":{"entity-type":"item","numeric-id":5387904,"id":"Q5387904"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$92DADBAC-3365-4396-A9AF-678D4DD5213D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$B895AE22-B03E-40CD-9268-F917EFF54EDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$06EC2A0C-F0A6-442B-9D8B-89AE1C162825","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7536e92384e11ec3ce8637ede805331f9e036d8","datavalue":{"value":{"entity-type":"item","numeric-id":3997095,"id":"Q3997095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$524D6D00-1A99-41F4-BBA9-22CECDD2CCEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bd7520de1b4bf1bc0bba49f7075996531473a953","datavalue":{"value":{"entity-type":"item","numeric-id":5477654,"id":"Q5477654"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$AA4B718A-FFC1-45B7-B93C-42E687B10759","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0edfa3788ed617f89af868a8290e7c98c185e04d","datavalue":{"value":{"entity-type":"item","numeric-id":3613427,"id":"Q3613427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$615C66B3-4E4F-4B87-AC4F-BB7BBCE75DCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef7ea17ddf2ff156a2c4fec2fd4f79b56138644a","datavalue":{"value":{"entity-type":"item","numeric-id":5493213,"id":"Q5493213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$4FF6363E-EBBA-4396-B11B-7E449983FFA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c35f4ebf8ba3be41685e193d999fe177c48a9c0","datavalue":{"value":{"entity-type":"item","numeric-id":4790648,"id":"Q4790648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$37ED5F6A-3557-4CD7-89FF-5CA24463D88D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"077640faa09a37374d345c86520e6868b04e6076","datavalue":{"value":{"entity-type":"item","numeric-id":2782479,"id":"Q2782479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$9940E8E7-14CA-4FE7-8D57-36E7D3310C3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df9fb4bc160a2caa739ce4a3c250258344d6a7c4","datavalue":{"value":{"entity-type":"item","numeric-id":2729073,"id":"Q2729073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$D1D96DCA-413A-4191-8072-D39DA529212A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9c714a7ce9338e0dc738398cae4dd66e54eec35","datavalue":{"value":{"entity-type":"item","numeric-id":4827596,"id":"Q4827596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$DEDEA53F-13F7-4C71-ADA4-A1B046195BD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"216559cea76cbd7bebdc584718098a2b0e882117","datavalue":{"value":{"entity-type":"item","numeric-id":5307074,"id":"Q5307074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$0F40BE9F-4EA6-458A-B51D-B3F190C9347E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a693c10013eb7bffb7ffbc0c1890644cc6a21fe5","datavalue":{"value":{"entity-type":"item","numeric-id":4809048,"id":"Q4809048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1006728$C2810693-7610-48E9-9127-412623EE61AB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f7be2a0d79aab18e703133df62b48210d31c6923","datavalue":{"value":"10.1016/J.JAL.2007.07.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1006728$F6353C0D-EC40-4875-A32C-32B760D879ED","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9b7d04a9ff7a9d025be95e1cfc5750dbf6e966c","datavalue":{"value":{"entity-type":"item","numeric-id":3543644,"id":"Q3543644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"be668f0df284fc6fd9d0cd5611d134a303137701","datavalue":{"value":{"amount":"+0.7461076378822327","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":"Q1006728$39298393-3A0F-4AF0-8700-99B4353BBBB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b3b0efa447d2f0bb1d07cfcfcea727ec3cbe250","datavalue":{"value":{"entity-type":"item","numeric-id":2280212,"id":"Q2280212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d90099e3f4abf33dc5c5231304d408464d12b99","datavalue":{"value":{"amount":"+0.7417488098144531","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":"Q1006728$7A1A95B5-2953-4C1E-B1BB-3B39644FDC75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56d606835397ced889225aa24646e03238343394","datavalue":{"value":{"entity-type":"item","numeric-id":3000661,"id":"Q3000661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e89e1eefff378e16d0db3f792eca3763dc452fb6","datavalue":{"value":{"amount":"+0.7387158870697021","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":"Q1006728$E09625FA-688A-43F8-AF60-9061DAD6267C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"28d5a8b545b5823d435e955696d0052fff4439c3","datavalue":{"value":{"entity-type":"item","numeric-id":2867932,"id":"Q2867932"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17ab5adc3b56ff31fd03104a4ea88d7bd04dfae5","datavalue":{"value":{"amount":"+0.7153218984603882","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":"Q1006728$3D994A98-8788-43A5-B65C-3EEAF27F445A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3866260072cf2859e4d234424d2722aea9ea4298","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f787ccb904a8f577d81f2287236ed41ee83882c4","datavalue":{"value":{"amount":"+0.710467517375946","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":"Q1006728$5A23CE3C-59CD-40A7-8D97-A85EF60E35B3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Integrating external deduction tools with ACL2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Integrating_external_deduction_tools_with_ACL2"}}}}}