{"entities":{"Q6589549":{"pageid":14200706,"ns":120,"title":"Item:Q6589549","lastrevid":55729909,"modified":"2026-02-17T21:48:25Z","type":"item","id":"Q6589549","labels":{"en":{"language":"en","value":"Initial experiments with TPTP-style automated theorem provers on ACL2 problems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7898672"}},"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":"Q6589549$18F85AAD-6285-4566-83B2-F56152053C50","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"72292b89372f5529cf7e39b5dfccc33c7a701549","datavalue":{"value":{"text":"Initial experiments with TPTP-style automated theorem provers on ACL2 problems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6589549$BADE937C-1E78-4F7C-A84B-6EB24CD07FCF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4cfa54ceaa76f200f8bf9566de4047d7b9e97656","datavalue":{"value":{"entity-type":"item","numeric-id":1785853,"id":"Q1785853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589549$44A63FE6-6B4A-4E69-9D55-CD4B3C196DAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589549$0A3DBCD9-C96A-4961-8DB0-B90B7BD28EA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6589549$C8E7E54D-803B-42DE-88C8-EAC0614746B0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"37c9edf3682f8ce3a18f69639bd1f0b09ec55ee0","datavalue":{"value":{"time":"+2024-08-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6589549$84492AB3-0690-4066-8BC1-C073324DC13A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6589549$2D14C193-9A0C-499E-84AE-C3CC2726AFEC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6e12eb4c7d2144b8e913bd2eea9f04c9101f35a7","datavalue":{"value":"7898672","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6589549$ECB9B3AC-FDE7-4436-90B5-AFEC5686E773","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":"Q6589549$6D189ADD-946F-4780-A84E-33CE460B00F6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3acd89bf1a885e8950aaa2f39bddd670d58aeea4","datavalue":{"value":"10.4204/EPTCS.152.6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6589549$731A0C20-FD68-4757-9447-41FE470BE86A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a780274f7d45e7496490ce3dfcc953566820d3ce","datavalue":{"value":{"entity-type":"item","numeric-id":3499763,"id":"Q3499763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f7b0fed164b5ef6dce9b4bc56879757fa7b51e55","datavalue":{"value":{"amount":"+0.7715581655502319","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":"Q6589549$B60AC780-354F-426F-A408-D8D4A643818B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f103237e1b4889a22b078c6687a2ac0c70875b","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0209d34f061771b8ccb02ba2aa8ed534cbb8a0bd","datavalue":{"value":{"amount":"+0.7667272090911865","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":"Q6589549$35A0F318-810D-478D-B2EA-0CE8144A218A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63c88c73eb0f33863fc007467a9962367e1e0911","datavalue":{"value":{"entity-type":"item","numeric-id":877826,"id":"Q877826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51040da3d060a8479a1f5f93c1e258ce080bddff","datavalue":{"value":{"amount":"+0.7497371435165405","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":"Q6589549$442F356D-3252-43A4-8F21-CEC0F0F66316","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b168262f9e1b4514313a24dfabf8223d2ad31a3","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4514c0bf0ee5f68b980ae055371c1e51f10bced0","datavalue":{"value":{"amount":"+0.7465740442276001","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":"Q6589549$B99B028F-CF9A-419D-853C-A1A373C2D40E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6b4440e24c330497025549da4d4dc8ba9f23acd","datavalue":{"value":{"entity-type":"item","numeric-id":5747877,"id":"Q5747877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"887f824bb2696234e1c2842b22e2025e341cb3fa","datavalue":{"value":{"amount":"+0.7374955415725708","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":"Q6589549$AA447E7A-CC3F-4284-864E-77188864289F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6589549","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6589549"}}}}}