{"entities":{"Q1404979":{"pageid":1415719,"ns":120,"title":"Item:Q1404979","lastrevid":67521924,"modified":"2026-04-12T18:34:27Z","type":"item","id":"Q1404979","labels":{"en":{"language":"en","value":"Limited resource strategy in resolution theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1970572"}},"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":"Q1404979$01135E17-B791-458E-B5A2-80C0044064B4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a72fc8b3c81e4be324d21ea285c77d644ec5c8d0","datavalue":{"value":{"text":"Limited resource strategy in resolution theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1404979$C99F973B-1F31-47D6-AA41-F22665D2707F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bf804afe91e09d3675a9bea98a1c1f884b803222","datavalue":{"value":"1023.68089","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404979$DAF1A3C9-22E8-4E4B-B795-E4E64C432CA0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6a0ecc9f5228f975307974b7d2fe5db407426476","datavalue":{"value":"10.1016/S0747-7171(03)00040-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404979$CF5B8457-09CB-41B2-A27E-CE2993DB6EF1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"79b982174bf75e7052721cc417e2d2d9f93c78e8","datavalue":{"value":{"entity-type":"item","numeric-id":1404978,"id":"Q1404978"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$1E014C13-B439-4FCD-B77F-9BA42AAB296F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bab2dfee53655d9cc8087a652185465cb178825e","datavalue":{"value":{"entity-type":"item","numeric-id":229754,"id":"Q229754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$931757E0-7D1D-4A17-82F7-EC5C18E6CE7C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$ECF98F63-23B2-4959-85AB-2FCAAC1364EF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"988a1f1f38c2f749de54c12ebc5774f827c2b17e","datavalue":{"value":{"time":"+2003-08-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":"Q1404979$2223F53E-5E1D-4EC1-8C5C-50D02EB0E38E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404979$1916D793-095E-4617-9A9E-6D5B721E1DCA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9ee005c4d8a187e905a152e112b28c6572d61ab8","datavalue":{"value":"1970572","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1404979$CD86037C-5F1E-4919-A3ED-437674FD105B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e97175fd5d747e7d34cbcc625e3abab53d84653d","datavalue":{"value":"automated theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404979$8C3458D6-F2D9-4565-BC2A-3E15219CDD7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3bc4e5082e4bd27c0afe02229842342d428e4e46","datavalue":{"value":"limited resource strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404979$82358A97-70E7-4642-8B23-1AD707E9968B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cfac5eb6431ec88e2a6e9bafbfcf7b49dda794fc","datavalue":{"value":"resolution","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404979$74BDF1D9-694F-4EB5-A1A8-12942DB47B56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f4aa81699d2d8275eafade555a6a1303d4941547","datavalue":{"value":"OTTER saturation algorithm","type":"string"},"datatype":"string"},"type":"statement","id":"Q1404979$E49E8693-5A51-4573-B0E9-6BBC2FFFEB66","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$01A705F3-5908-41BB-AAA4-12E570410215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$846E048D-BBAD-4DEB-9FA2-87EC5D3F51AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f1ae8e244d27f4e93f1981ec80f87d04dfe89da","datavalue":{"value":{"entity-type":"item","numeric-id":31438,"id":"Q31438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$DCE9F9DC-E6B7-42D0-B8A0-53291032973F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$B47AE333-5A89-4B9E-AC95-A8FA3AFCDDAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4a761178b05ceb8505a589f51ea41c7640322dd0","datavalue":{"value":{"entity-type":"item","numeric-id":33154,"id":"Q33154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$8C87176A-747C-4764-B59E-923D1EE634D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"497739b1d588e442d5b7ba6bb4cccae512fc3231","datavalue":{"value":{"entity-type":"item","numeric-id":19196,"id":"Q19196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$54C0560E-1DA3-47B1-8533-771025DE95CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$AAF37FC6-BFE2-4757-B2FB-7A37DFD05367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$C25E29AF-3EE4-4009-9E56-C2148E4462F3","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":"Q1404979$F3F7FDDB-D198-4B62-A4D7-B2693E2429CF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf670e64a6cf63cb8d60b11cd930f4ce42cede15","datavalue":{"value":{"entity-type":"item","numeric-id":4524770,"id":"Q4524770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$539A059A-96BE-46E7-AB09-D3D5CDA89D27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43218a27def39b9a64d8410d1795d8997255e252","datavalue":{"value":{"entity-type":"item","numeric-id":1294673,"id":"Q1294673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$C53BB683-95E3-4132-A86B-8A7BA86B2EBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cff8a314d9fb157a7d13b3fe1123cbf96f16e53","datavalue":{"value":{"entity-type":"item","numeric-id":4539610,"id":"Q4539610"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$5443C195-EF4C-4760-8F41-F74545C937D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c061dab185fe1bef51da7d9346e274bd625a1e8","datavalue":{"value":{"entity-type":"item","numeric-id":4539622,"id":"Q4539622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$0EEC670E-C520-450C-B896-036DB489CE72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3acb227cc182218e10ebdc1a3b0a4f5f641d466","datavalue":{"value":{"entity-type":"item","numeric-id":4539621,"id":"Q4539621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$1B9E2145-AC75-47B7-8E00-75757C040477","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f707d41b44671464c5d9fbd310386196c74d6c07","datavalue":{"value":{"entity-type":"item","numeric-id":2751378,"id":"Q2751378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$13A1046D-F411-452F-AFE6-E63CED60CEBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c2bbb140c4dbfa368d507d72919bce6409b4ee6","datavalue":{"value":{"entity-type":"item","numeric-id":1977578,"id":"Q1977578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1404979$979B7B74-7AAE-4810-BD52-1B5B427761CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eeecdb134ef718397551eab16d66c08f458815a9","datavalue":{"value":{"entity-type":"item","numeric-id":3043806,"id":"Q3043806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b747a2a9d439124bdfbaf1b10475c80b63cfc84","datavalue":{"value":{"amount":"+0.9339349269866944","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":"Q1404979$C3B3E252-E2DD-4BB6-9377-24E42F22292D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3328acb14c381645dbb1f9eb31b744a4a34bbbc0","datavalue":{"value":{"entity-type":"item","numeric-id":5210762,"id":"Q5210762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3eab98a8c12b8288168bb0166f7096a5cdfb4e34","datavalue":{"value":{"amount":"+0.7603501677513123","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":"Q1404979$1EF75A25-BB16-4D83-91A6-8D9EB2ED38F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1977ce75e4c66a6e986ece8bd137815f9305537","datavalue":{"value":{"entity-type":"item","numeric-id":4345253,"id":"Q4345253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02786a189ce6262c40701f2e9c7e681a8ecd2a03","datavalue":{"value":{"amount":"+0.7549556493759155","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":"Q1404979$023C9388-1D16-4633-A82C-F450A7328D15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fde046d0deb27a80459fc157105f541312bedc56","datavalue":{"value":{"entity-type":"item","numeric-id":3499018,"id":"Q3499018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02786a189ce6262c40701f2e9c7e681a8ecd2a03","datavalue":{"value":{"amount":"+0.7549556493759155","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":"Q1404979$F41C8530-BB01-4860-8528-E874ABC4483A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48a3d434253ed919faa661b14e883ac27b635cfa","datavalue":{"value":{"entity-type":"item","numeric-id":2751353,"id":"Q2751353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"194bd70e933dcb08f08e5d9a2a8ef971b188b057","datavalue":{"value":{"amount":"+0.7284688949584961","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":"Q1404979$AC1970E4-6BA9-4026-B2C3-56AF4852628A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Limited resource strategy in resolution theorem proving","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Limited_resource_strategy_in_resolution_theorem_proving"}}}}}