{"entities":{"Q6492544":{"pageid":14071317,"ns":120,"title":"Item:Q6492544","lastrevid":39782643,"modified":"2024-12-30T18:47:12Z","type":"item","id":"Q6492544","labels":{"en":{"language":"en","value":"Fully reusing clause deduction algorithm based on standard contradiction separation rule"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7838186"}},"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":"Q6492544$64F4B9B9-AE7C-41C0-AB4C-6A23B3011AF7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"72c400daf9ae73692a962d46fab6a31eba98cdda","datavalue":{"value":{"text":"Fully reusing clause deduction algorithm based on standard contradiction separation rule","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6492544$14B8FC3C-218C-484E-9CC8-2E2969781FD3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0a1c39d4d61829b3a9f85f1e8cee305978d02d54","datavalue":{"value":{"entity-type":"item","numeric-id":5163183,"id":"Q5163183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$A2DFDFEE-5803-4616-9E07-7FF1CAA641F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ee6429993c4b83380d2aa1a3eca2b98f393effbe","datavalue":{"value":{"entity-type":"item","numeric-id":209286,"id":"Q209286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$D88035AD-66F5-4C43-87DA-08E7EE51CFE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3a5677de8d09cf5673a2960a3a4d5abd93c72250","datavalue":{"value":{"entity-type":"item","numeric-id":209287,"id":"Q209287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$824BC9B5-A0FE-49E5-810B-F5CC5CA7CBE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad21a50f8b52ec1e6ac5232064753ecf36423939","datavalue":{"value":{"entity-type":"item","numeric-id":498107,"id":"Q498107"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$7F292B0F-FFF1-4F0C-BDDD-7ADE44D46041","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4ea5350c94d5cd96d96cbc78d65795c9b56975b0","datavalue":{"value":{"entity-type":"item","numeric-id":849939,"id":"Q849939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$7BCD6DC8-929A-44CF-94A2-7818CB2A06BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d356adca328e50aa4488b6ecdb1b28ac263ee6b2","datavalue":{"value":{"entity-type":"item","numeric-id":2333857,"id":"Q2333857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$BD9B5533-D4D9-4353-8DDE-85306E90EAEB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c144f0fb88440afe4b13555aedcc8676a016b6d2","datavalue":{"value":{"entity-type":"item","numeric-id":70466,"id":"Q70466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$8233A715-4355-4314-81C0-3EE70F6AFC55","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61877e84ba989d20dbe6baf29fb8934f5cbbd9f7","datavalue":{"value":{"time":"+2024-04-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":"Q6492544$0907F253-D2F2-4C21-A876-79D6F66403D6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6492544$820519AF-C132-4070-94D8-0C485DFBC4A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5dc47a80375051b61326aef30653f59f9c0922b4","datavalue":{"value":"90-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6492544$ED76E69E-B54B-41A5-89C2-DEFBA4BB7B33","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a0c21074a51ece066d88a44bdc3a59433c972ae5","datavalue":{"value":"7838186","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6492544$B40FA6B5-EA47-4986-8D6B-1BA01D4FBD99","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$74444ECD-57A4-4E4F-90B0-B3563B505DA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6e4b960a9ec2fd7ea13017247cbcc0a363da4ec1","datavalue":{"value":"ATP system","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$DABF7EC0-8425-45DC-9880-7FDF987A35C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"93cbbe3aacb0282d348cb5e7d78e394a1a6097ce","datavalue":{"value":"inference rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$5BC72EA4-5881-4AA9-BF41-186D1EE7FBE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"75060658962a9436cf22f58601253eb29070263e","datavalue":{"value":"deduction algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$CC977998-2B16-4D8D-9D6D-B290A5858C50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a28d8d5227c4b44523fb5f2b115802bd22cc984","datavalue":{"value":"standard contradiction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$CD977582-6075-4DA0-9B19-C3D28FBB2645","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"35948fd6c1c56c721383ef36d153f4644f15ed89","datavalue":{"value":"S-CS rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$2AAB386E-A431-490F-9973-6046B6167472","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"849fd7c9ca92686500c5ea19f093aaae755705b4","datavalue":{"value":"vampire","type":"string"},"datatype":"string"},"type":"statement","id":"Q6492544$55ACF6BD-4592-4BFF-923E-B09A401FF386","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":"Q6492544$CD305395-88BB-4BCC-A12B-AC179CAFA5E1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4c41debdc70e73ca1fe31e7802144d1e5b9ef9a","datavalue":{"value":{"entity-type":"item","numeric-id":3308161,"id":"Q3308161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$9DBAEA2D-8FD7-401D-804B-218436878096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adbfa02ab4b7e0bb252f5a5604936a94deac79e9","datavalue":{"value":{"entity-type":"item","numeric-id":3847756,"id":"Q3847756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$85E7B329-6637-4D3C-90DB-3D6AB5263C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e44e9e532a60b0c2fe7f69fc24b91b25cb2cddc4","datavalue":{"value":{"entity-type":"item","numeric-id":2305434,"id":"Q2305434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$D92EE295-032A-434D-9173-9831EA7524D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca2db2cf1ca162d8b25f8aa0d21796f35245b1e5","datavalue":{"value":{"entity-type":"item","numeric-id":6108829,"id":"Q6108829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$6DFD77A3-0BF0-4639-AC81-193DF9009F84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1529751d26cf89fd2faa553de05698ce2ba38233","datavalue":{"value":{"entity-type":"item","numeric-id":2817929,"id":"Q2817929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$B0FAC249-0DC4-47E1-960E-1404246D904F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35a75f053a353053f076c4579a8bd7588f50e677","datavalue":{"value":{"entity-type":"item","numeric-id":3568228,"id":"Q3568228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$4E7CBCAE-9FE3-4D95-A172-4A1754A38BB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8674a26153ce786fc142cbca9d495f9ca891ee8f","datavalue":{"value":{"entity-type":"item","numeric-id":2996159,"id":"Q2996159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$4649D6F7-C60E-4B70-8141-8C1BFDBB2CAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9297b6a91a7c29eb2b70ce4159ebd40915c17240","datavalue":{"value":{"entity-type":"item","numeric-id":2305435,"id":"Q2305435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$D8C0DC6D-176A-4907-8912-EE6365E95906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"678ab028e64aa47294ec33138952f2e29114a933","datavalue":{"value":{"entity-type":"item","numeric-id":2817933,"id":"Q2817933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$780FCCC5-20BE-42E6-8ECF-7E412AAD1DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f62ebef9379ad97d2bdc3c2e7f5717f221d056cb","datavalue":{"value":{"entity-type":"item","numeric-id":5514129,"id":"Q5514129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$A5BBFD64-A120-4D4A-BE9A-1062BAB098B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33890b7faad584193275d91a4cd4d3b147aff5a7","datavalue":{"value":{"entity-type":"item","numeric-id":3541709,"id":"Q3541709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$7AB51C9C-A9B9-4AB6-83B4-A842146D0976","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cb8e50e6c3bd60a9a9a59407cf30e8e788baa4","datavalue":{"value":{"entity-type":"item","numeric-id":3618853,"id":"Q3618853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$6D3F5B87-0BE6-4261-B75C-37742103AE6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f20d0265bfeffe57194cce3d2a09764d8168afa","datavalue":{"value":{"entity-type":"item","numeric-id":3454079,"id":"Q3454079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$ACB9096F-649D-4FE8-B9E5-2C9F860A0D15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dbf5d4c6cedd5848e03816494729378cde53a8e","datavalue":{"value":{"entity-type":"item","numeric-id":2551698,"id":"Q2551698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$68DD4B53-BD40-4545-B738-88A001BE9D1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f771f551f48b2f2d21f6f2011008cb21eb26e492","datavalue":{"value":{"entity-type":"item","numeric-id":5538933,"id":"Q5538933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$56EFBA3D-B775-4E8D-9D05-17E48B0BB5A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cf2a467582e2ce551e8d6f09e937481123bd1d1","datavalue":{"value":{"entity-type":"item","numeric-id":5049022,"id":"Q5049022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$E3B6345B-984A-44CB-897F-EC12F0AACDC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3229ea41a0e4cb12db1be06015db0374810e3bec","datavalue":{"value":{"entity-type":"item","numeric-id":2305433,"id":"Q2305433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$AC57CC0C-1DF1-41D1-AE20-5582F0312ED1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87e7d3f8aa3a56ebc7274d4e2273eecc7a09f3e1","datavalue":{"value":{"entity-type":"item","numeric-id":4529543,"id":"Q4529543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$58177325-6560-497D-B298-DCC480588440","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e861cd1c39178d9f4fad683e1f336b1d3e6d6eb3","datavalue":{"value":{"entity-type":"item","numeric-id":5307048,"id":"Q5307048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$62F41B12-0B6B-4552-A1A7-451F1BF2ED13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"33ec6a38e62b229158ba6796c81864271d359e34","datavalue":{"value":{"entity-type":"item","numeric-id":2405255,"id":"Q2405255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$06B99BEF-AAD6-4385-A60D-3F67A07C9181","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8ecea4c5d53ccd7f3b9e49fb12de3d378b37cc4","datavalue":{"value":{"entity-type":"item","numeric-id":2305419,"id":"Q2305419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$720AFEE9-DE57-4493-8CE6-8488BCE9BBEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de61fdcccb88d2f352f7a27c4d3d90e13a3d174a","datavalue":{"value":{"entity-type":"item","numeric-id":2198231,"id":"Q2198231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$CADAB761-BF05-4383-ACDD-B4903267E282","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d27fb393ac8f67685d6f7819a6abe6c2becacf74","datavalue":{"value":{"entity-type":"item","numeric-id":6086313,"id":"Q6086313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$B8F63FCD-0AEC-4832-9BFE-298618EBCBF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f82f0f40ab66cf033c5a229880b34de6b2284f9c","datavalue":{"value":{"entity-type":"item","numeric-id":1694574,"id":"Q1694574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$1132385F-09EC-4A0F-8F9C-A546E2DBB670","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d4acf12f6f2468476af5b80237d12aa6e90faaa","datavalue":{"value":{"entity-type":"item","numeric-id":3066085,"id":"Q3066085"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$EE3F21C3-E2E7-49D3-95FD-D651AC1FFDCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"55cea594f37031bf55b82bc70b085187bfc9c6b5","datavalue":{"value":{"entity-type":"item","numeric-id":2096461,"id":"Q2096461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$EB2B9609-4A3A-4335-A6AB-0BCB19F72093","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6aae6d5aa9f7ea8a6c151199cc5229d272d48da","datavalue":{"value":{"entity-type":"item","numeric-id":2233504,"id":"Q2233504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$98E1FF25-7DA4-481E-B07C-70C066D51088","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63d7f3718748c1529f8e53c69f24865fbcaada27","datavalue":{"value":{"entity-type":"item","numeric-id":2305438,"id":"Q2305438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$A6BE84D9-3C5B-4484-BC13-8F11AC2C73E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8bd554443d4def680b4aedb7a5e010af4f212d5","datavalue":{"value":{"entity-type":"item","numeric-id":2128804,"id":"Q2128804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$7170930A-E426-40AA-8912-D18AC4E6BCB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86702a2c27a2e419f342f805a15c601a0c303b4b","datavalue":{"value":{"entity-type":"item","numeric-id":1891262,"id":"Q1891262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6492544$6247B459-F4BA-4131-8503-AFBF67F538BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"02548e021aa0e5511006e9d628a4f0f1fba99606","datavalue":{"value":"10.1016/J.INS.2022.11.128","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6492544$61F4D6C9-91BD-470D-9210-36918B86E5C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6492544","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6492544"}}}}}