{"entities":{"Q6535368":{"pageid":14146511,"ns":120,"title":"Item:Q6535368","lastrevid":57344271,"modified":"2026-03-30T14:07:42Z","type":"item","id":"Q6535368","labels":{"en":{"language":"en","value":"\\textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7777314"}},"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":"Q6535368$EBA71806-B4D4-4819-B70B-32734D434703","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"817c9dfe69a717d1a73b582199e446313f1b83d9","datavalue":{"value":{"text":"\\textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6535368$8B216B1F-6B67-4F7C-88AE-8CC8F6F962C6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8d5cc766ccf1a66f18bbd922d208848a2135c390","datavalue":{"value":"1543.68395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535368$8D3D2644-1481-48FD-8266-6C1A952A1F87","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9afea78cc28719421c21a8d1dc7cf795b9efbeaf","datavalue":{"value":"10.1007/978-3-031-30823-9_19","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535368$E04B93E2-5C16-4AD6-B996-65551155092F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c0270c5f09013fd16c6b2445a8928308c49d0b14","datavalue":{"value":{"entity-type":"item","numeric-id":608193,"id":"Q608193"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$9EE57249-8D93-4F57-9A8D-12D500026E0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"94896fa27c3ea62740b55326a00c2f3dc2685f84","datavalue":{"value":{"entity-type":"item","numeric-id":2104492,"id":"Q2104492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$71FBC532-639C-45FE-AD23-29EC6466D935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"20dd65c281e6e985b6ecebe81cd888c922b7f37c","datavalue":{"value":{"entity-type":"item","numeric-id":1799120,"id":"Q1799120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$FB27A64B-85AC-48E6-BDC7-713A10AD500B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"370dd048328bd35e66746fcb16650fb884273700","datavalue":{"value":{"time":"+2023-12-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6535368$017B882E-9C32-4427-9E29-7D2130864C9F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535368$E33167FC-381E-4C57-AD46-5403C5135306","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535368$E58D88B7-BB3B-4BDB-8B9E-EF64E33DD529","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f0a8cd5e4495b52d450c34611bf18ff85188e6c8","datavalue":{"value":"7777314","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535368$A456166F-8C9D-4D0C-A3CB-D78EC15CEAFC","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":"Q6535368$F7DB0CC4-5BB8-4F12-B746-43C742724B87","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb15445443b7a8677c7ef043ed8530f20d54b0c3","datavalue":{"value":{"entity-type":"item","numeric-id":3100209,"id":"Q3100209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$65BA54BC-535C-4832-92EC-ED70AB8339D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8bbbd10679bf2d321eb9db870479cc35412cbd39","datavalue":{"value":{"entity-type":"item","numeric-id":2104495,"id":"Q2104495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$56133CC5-6342-42FC-977F-EA3983A5241D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6788f8c83d5a5db6237942eed0df1dc9fb4fc24b","datavalue":{"value":{"entity-type":"item","numeric-id":5919479,"id":"Q5919479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$CEBEB124-5E02-44C2-8C00-D2E6AFA53928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a5f7ec14119349332290c2a3236ae73e2231fc2","datavalue":{"value":{"entity-type":"item","numeric-id":3176369,"id":"Q3176369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$29F0CD9B-D6E0-4CEB-88FC-5A934593CE94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f6a505c48f7ed8fbc36053c87307f799e1a7f54","datavalue":{"value":{"entity-type":"item","numeric-id":2351158,"id":"Q2351158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$34FCEAEC-73A0-4DC6-A451-4FCCCB5134A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efeed698c61c9d4088905eab8917123fdb73bb41","datavalue":{"value":{"entity-type":"item","numeric-id":3100212,"id":"Q3100212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$DA261CAE-95C2-4401-AB28-B69CE0B92150","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea4acb53c6aa01f94c371c1488d0c79ed81e1ea7","datavalue":{"value":{"entity-type":"item","numeric-id":1637915,"id":"Q1637915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$60D75EFC-9B7D-4409-934C-37E3010C1C2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0ecda2530a74fd3b958fc170aad75894016b80e","datavalue":{"value":{"entity-type":"item","numeric-id":3541720,"id":"Q3541720"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$559C5D77-214F-4D34-B4A0-39BF70EF2193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b61ff436ad097e7899027abdd6e0c42fca0ee2","datavalue":{"value":{"entity-type":"item","numeric-id":2164216,"id":"Q2164216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$9E916302-0CE6-47F2-8FE1-957F95AB2941","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bbed57047570d97d4afd4eabda171670dfd2346","datavalue":{"value":{"entity-type":"item","numeric-id":2703808,"id":"Q2703808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$944DAD34-353B-4E86-8800-C67F998E770A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"00c2d672d21d4d5af646f31d9599e67b8b6b153b","datavalue":{"value":{"entity-type":"item","numeric-id":1663234,"id":"Q1663234"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$52AFEDDD-B992-4506-ABE2-86C30176A463","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$A575D0DE-F3AD-4946-88EB-E398FA09D78F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c9e38395117f774ba9617661fcca711bd13f7ff","datavalue":{"value":{"entity-type":"item","numeric-id":2818042,"id":"Q2818042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$2DA3C7D2-05E3-40B0-B99D-CEAEEFA98C3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"975126c2667d6964e52988e556bf8223ff836bfd","datavalue":{"value":{"entity-type":"item","numeric-id":3883564,"id":"Q3883564"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$75C1FEEC-629B-4E8F-B2EE-B84BEA9D3449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79db93a0bb311f56c816d6ffc92dd7b60e23250d","datavalue":{"value":{"entity-type":"item","numeric-id":3455223,"id":"Q3455223"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$CE6FB02C-B8CD-4810-877B-F8383E711E7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"951b0d64fa001352bd85440b66bf6883d66476f8","datavalue":{"value":{"entity-type":"item","numeric-id":2050109,"id":"Q2050109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$D4FBF80A-A029-4C6E-B28D-F7CCA0F9179E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f24266047ac8ffcefe32630c940ffdb70489bec0","datavalue":{"value":{"entity-type":"item","numeric-id":2891429,"id":"Q2891429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$952CAFDE-D967-4DBB-ABB0-662F20D53867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61d2acfca0f5dfd32b373cf14812fef011284ac9","datavalue":{"value":{"entity-type":"item","numeric-id":2055877,"id":"Q2055877"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$9B166975-01BC-4B09-90DF-3D50A8BC65BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee09e75a430fc0be911c9a36f98899b21bf0296","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535368$1DE4E8C2-17AC-4B37-9BE5-28A98577CF8B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b25840e9689e28a5767a31e8370e4b859c5091dc","datavalue":{"value":{"entity-type":"item","numeric-id":5458346,"id":"Q5458346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6e7055203836fc23d2b7135b0989edf9a9dc57a7","datavalue":{"value":{"amount":"+0.737356960773468","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":"Q6535368$0B94B983-F015-4044-9A67-DCEFBAD8480D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dc4a898c2ce53e9d3b4432ba9d09cae8e716f24","datavalue":{"value":{"entity-type":"item","numeric-id":2441776,"id":"Q2441776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ad9ed2fc3c8ba1e77c0b7e1f8cc4c7db11a210f","datavalue":{"value":{"amount":"+0.7133419513702393","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":"Q6535368$3A120141-28FB-45A1-B39D-DDEE12BA1AE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6909fca2f047c70d1bf0830c72b5b2c4810826f","datavalue":{"value":{"amount":"+0.7006063461303711","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":"Q6535368$1ECBF61C-51BE-4715-988E-19C2822E0D74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0b4f75f494f6421c325356fd1ed820027bfc297a","datavalue":{"value":{"entity-type":"item","numeric-id":5747649,"id":"Q5747649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed24098cab585fb234ec54dff1ac07d63d24c97d","datavalue":{"value":{"amount":"+0.6990600824356079","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":"Q6535368$8D4F5D09-11D5-4189-937E-74F727153EB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9541118d0e80b14a3878d56a9fa40c6f059cb57","datavalue":{"value":{"entity-type":"item","numeric-id":2233509,"id":"Q2233509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96e25391f0cdd04ff6ece1697079d94964c25ffb","datavalue":{"value":{"amount":"+0.6986983418464661","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":"Q6535368$3ED3AA73-1203-4F1B-9A47-4119E4AE177B","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":"Q6535368$5D3876EE-3282-4C2C-A648-684691CFB1C4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6535368","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6535368"}}}}}