{"entities":{"Q5916290":{"pageid":8032822,"ns":120,"title":"Item:Q5916290","lastrevid":41166138,"modified":"2025-04-18T15:25:50Z","type":"item","id":"Q5916290","labels":{"en":{"language":"en","value":"Formalizing Bachmair and Ganzinger's ordered resolution prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6958094"}},"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":"Q5916290$950A62D0-3944-410D-A046-ABC633F55465","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bbcf2c8ae39c653dcaf1e1fc1c5c1c84bd7b6dae","datavalue":{"value":{"text":"Formalizing Bachmair and Ganzinger's ordered resolution prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5916290$27C14B6E-EFC5-4438-84EE-1FFA1925A2DB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ac6a8b1709831a288d9fb85d364e1fa9f2f79ce0","datavalue":{"value":"1468.68306","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$6499499C-4D0A-43C7-82BC-1816DF44E792","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ff817f03565947926f20214d356d7ce17e9a8edd","datavalue":{"value":"10.1007/978-3-319-94205-6_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$711B17FE-87D0-4537-BB64-6F612E47CF0A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"38e62085f18fee17b0db8da8d8ee5d2427f90091","datavalue":{"value":{"entity-type":"item","numeric-id":1663241,"id":"Q1663241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$DEEFC433-B816-42E7-BED3-5A2C91098A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"42c29c686dffd678d9f155b05a4a1aa93e85953c","datavalue":{"value":{"entity-type":"item","numeric-id":287335,"id":"Q287335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$1B8361ED-924E-4AEC-9B6C-0D3242C57A91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"157dc0abe360dacc915db0769a2ed352a42201ad","datavalue":{"value":{"entity-type":"item","numeric-id":1687534,"id":"Q1687534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$2047A574-7A09-462E-ACC8-9C6C975A1268","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ecde3ddf4f96a8da457aeb906b2979614b354694","datavalue":{"value":{"entity-type":"item","numeric-id":293310,"id":"Q293310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$717C12AF-6738-4721-B835-3D9E522C7A4B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$845AE22E-FC96-44A6-9A4D-0BF2C52606DD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5916290$BB0F822B-B6D8-49A4-AF38-72B90ECA8D38","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a24047c6d5a8082bd9fa931d703a63ec424be0c0","datavalue":{"value":"http://hdl.handle.net/1871.1/09bae484-e3f3-4ea4-a2a6-77e59679a235","type":"string"},"datatype":"url"},"type":"statement","id":"Q5916290$0AE0F5F6-CFA3-4932-89F2-37BC1D64A9B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$D63EA359-2714-4C46-8578-651DA3C556FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$4EBFA23C-8F7B-4658-B0EA-C1B8BFD5076B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$8C45301E-E56F-4F88-B9C3-7C003D79B99D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"85b04decfdcbbdd756e76dda11aea988982521dc","datavalue":{"value":"6958094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$72B1B18F-7D12-4910-8179-63EB445BBEEC","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$B35E3C90-129B-4768-AE8B-3908055941E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8e7deacad56e3bf59f522de6c1fa96858f2fd494","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$BC5DC165-9CCE-4909-BCCA-B6A14D4DDBEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$49D8FFCE-538A-4C34-BC03-F84C570036F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$EE42A611-AF41-4801-9238-438CE163498B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$F79336A3-667E-4E56-A6F5-7F2BAA1C93AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f3dc49212bb1ac953b456b7ee6d37c17258b97b9","datavalue":{"value":{"entity-type":"item","numeric-id":18543,"id":"Q18543"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$613B4270-1424-4AE0-89E2-E48EA6E618C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4a9f47cfb1039b607df8414b949b308b844e18d","datavalue":{"value":{"entity-type":"item","numeric-id":40285,"id":"Q40285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$5772AEF7-B38C-48BF-8843-EC6B253F3FB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$83476A63-8617-4661-83BE-BE0C6DB02BD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1cf431acf94a219782873a4ece8089be737690cf","datavalue":{"value":{"entity-type":"item","numeric-id":40349,"id":"Q40349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$163AB828-3271-4068-B779-9A0026FC0270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"90c7c18880caa813a6bdace0f373d3dec3147690","datavalue":{"value":{"entity-type":"item","numeric-id":40350,"id":"Q40350"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5916290$BDAB618A-EBC5-498C-A995-0E25D4CD578D","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":"Q5916290$CB48B4FF-EBF5-4E75-A89A-1A80309B9944","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"189833dbfafc8f1e58fd328908c1b87ef2f05d3b","datavalue":{"value":"W2787490662","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5916290$B9D21488-8F31-4C09-9151-C8E8193A0CD7","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c1e2f265ef0cb2d6386b1ca06a2b615173932cf3","datavalue":{"value":{"entity-type":"item","numeric-id":5919011,"id":"Q5919011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f5bad60f5d71e07f84653e70422d32de406082f","datavalue":{"value":{"amount":"+1.0","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$EDE0B88B-22BD-4E3C-ACC6-FB23CE1874B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0275d8299033c9f99fabb4193ffab91462b27ae9","datavalue":{"value":{"entity-type":"item","numeric-id":4255506,"id":"Q4255506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d738deb981e68d3565d3b1a060bbd01232948ca","datavalue":{"value":{"amount":"+0.90352625","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$D18F1A4B-F7D7-492A-B983-2CA65D8F7B01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1703b32a2b77d0843308ad39e4abb09b5e4bc888","datavalue":{"value":{"entity-type":"item","numeric-id":2829269,"id":"Q2829269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16cf937cf3a57f12c101e6d06c6c5732b44f76ce","datavalue":{"value":{"amount":"+0.89626384","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$1D83ACA2-CD4E-4D4E-9B19-9E8C11C3DFDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bbaec2746b1bccca32932fae8a20b45338558eab","datavalue":{"value":{"entity-type":"item","numeric-id":1663242,"id":"Q1663242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16cf937cf3a57f12c101e6d06c6c5732b44f76ce","datavalue":{"value":{"amount":"+0.89626384","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$EC40AF46-61C1-4436-BA37-F0249364314E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2bc88718a305d147397faaf7899d51ccdc2bb5ca","datavalue":{"value":{"entity-type":"item","numeric-id":4647496,"id":"Q4647496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b1119dcac389e7a2103875528291f6cb4016254","datavalue":{"value":{"amount":"+0.88030446","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$4AB9E9F9-8237-4169-B551-BEFC1D2FB7F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebc099bf621adc8a302704653b45f0029a43f506","datavalue":{"value":{"entity-type":"item","numeric-id":636273,"id":"Q636273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"193498943ff3a33f2d31878291ca48508e7a256b","datavalue":{"value":{"amount":"+0.87752724","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$3D2F9E6B-A4F1-483A-8873-0C7F45B3DD7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4821d184ef83e5752c967d173acfc4a04c2e4cff","datavalue":{"value":{"entity-type":"item","numeric-id":5434504,"id":"Q5434504"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"193498943ff3a33f2d31878291ca48508e7a256b","datavalue":{"value":{"amount":"+0.87752724","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$943C444E-BB0D-46CB-8888-CE5915FBDD1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"97cdde3ee7f21322dfd39feee80b7b145a35bf7a","datavalue":{"value":{"entity-type":"item","numeric-id":4207882,"id":"Q4207882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc8e7ffc3506fb8654f267f7a6bc5bf2a920a7cf","datavalue":{"value":{"amount":"+0.8762348","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$86C85AE4-05AD-4521-BA56-02CCD44B0D57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fb2995e256b76dcca4a3a251f2a6ae52e3e3c4d","datavalue":{"value":{"entity-type":"item","numeric-id":4299008,"id":"Q4299008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04f06726525f8e5a7ee2957b1c6ef3889aadf0cb","datavalue":{"value":{"amount":"+0.869303","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$05962A6B-00DB-478E-B19E-4CE4E072A13A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b79ff46c62eb19ec3b05b87662de25751c1c66c8","datavalue":{"value":{"entity-type":"item","numeric-id":1881219,"id":"Q1881219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8b6d45f8c3a3ae697a8eb63eeac4f2e3d5b7d0ce","datavalue":{"value":{"amount":"+0.8674549","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5916290$A71CE835-5096-4100-AE01-81F264CA5D2C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5916290","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5916290"}}}}}