{"entities":{"Q876046":{"pageid":877894,"ns":120,"title":"Item:Q876046","lastrevid":65018835,"modified":"2026-04-11T23:46:29Z","type":"item","id":"Q876046","labels":{"en":{"language":"en","value":"Fast congruence closure and extensions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5143639"}},"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":"Q876046$060E6D32-6978-4C19-9F0D-1049AA5EB93C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d52cda56da78e9e6f6556b4d94a5b8499d3b6dab","datavalue":{"value":{"text":"Fast congruence closure and extensions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q876046$AEE5965F-76FE-491C-B8F9-1BC957DF66F0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a28f6608357c6625e666c5dc65d8d0675de911d1","datavalue":{"value":"1112.68116","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876046$00ADBC9C-013D-48D6-9018-D35864592BD1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1e6a58ff964b9ca97414f0c42659717fa8e6fc43","datavalue":{"value":{"entity-type":"item","numeric-id":475169,"id":"Q475169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$7663D5CA-D0F0-430E-AE49-2FBD856903AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cfd1da8b09a3144b32ef026d1d9b2bca68560b37","datavalue":{"value":{"entity-type":"item","numeric-id":438574,"id":"Q438574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$8DADE633-67D3-45E3-A64E-62D7CCCB6F58","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$E0E44E63-5DB6-4173-8869-1729BA854378","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d952bbb2d53d4bd5a9de3b9e090440b84b7e8929","datavalue":{"value":{"time":"+2007-04-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q876046$EAA84706-2A2E-4AB0-9601-22273AB7DA1E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876046$317083C4-AD63-4C21-8A49-91EFC5937A43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876046$990A4BCD-5002-4B80-A900-9464BEEB8A11","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5e98fef5d93789471f339f57a5279c244a171cac","datavalue":{"value":"5143639","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876046$ABFEC9A1-255C-424A-8F65-8ED73C337484","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dfd2ae52b3325778b0c72742b08c947a3c4a2c65","datavalue":{"value":"decision procedures","type":"string"},"datatype":"string"},"type":"statement","id":"Q876046$8B881A5C-5AE6-4D5E-8FED-6366079B0357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85f840ce5119480b895ac664a10de6f0a19316ae","datavalue":{"value":"congruence closure","type":"string"},"datatype":"string"},"type":"statement","id":"Q876046$E7D6A087-7A3B-4DBF-A0D0-248FF9A1637F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca82b8126faca2bdab3ffa77f0c22600be2e10e6","datavalue":{"value":"equational reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q876046$2F88E008-753D-4D3E-AA50-D287905777B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q876046$597D01E4-869C-4B37-AD4D-ED81A471BDEB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$D68A3298-52AE-4331-AC1C-203861C53B0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"842bcffb0bb918fd12447e4f670f8dc61d68f929","datavalue":{"value":{"entity-type":"item","numeric-id":21432,"id":"Q21432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$BE83C9B8-D6AF-4A84-80DA-FB2F54DC7341","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":"Q876046$0A4B4435-F5A8-4E8A-9D63-4635C3A96ADF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6dd4532e17b20edf8500b4906285ae9bd344ba8e","datavalue":{"value":"https://doi.org/10.1016/j.ic.2006.08.009","type":"string"},"datatype":"url"},"type":"statement","id":"Q876046$54ACB83B-23C3-43A0-A39F-C5AD2001364F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"df35f3829fae7196dd98e0133f16b47444b5b9c7","datavalue":{"value":"W2138865396","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876046$F12693AD-43A8-4603-8630-81CB5046BA8E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ca6a116cda218a5a5ba933b4a80a76fb1eeb6a2","datavalue":{"value":{"entity-type":"item","numeric-id":5717462,"id":"Q5717462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$3C298854-E949-41D3-AE7B-7636D554E138","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f71dd5571a3c1c99537e11b357ad1449f45692c1","datavalue":{"value":{"entity-type":"item","numeric-id":4809056,"id":"Q4809056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$77EF420E-9153-4313-ABD7-7827D569EBF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dc64d6d31493ac74da4f6c177f509ec4a9d4b14","datavalue":{"value":{"entity-type":"item","numeric-id":4804899,"id":"Q4804899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$36FFA0F8-2765-4140-B996-C9E6CDB05E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"625f6543cb45ef040d1e85336980be3f05f00677","datavalue":{"value":{"entity-type":"item","numeric-id":5900690,"id":"Q5900690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$81766791-FAAC-4A2F-BFF5-477ECD435008","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da96dfa99f70c6b2b69c48b417a516b8fa851830","datavalue":{"value":{"entity-type":"item","numeric-id":5312898,"id":"Q5312898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$F9BAE3BD-0ED0-44E6-A636-8DFD163EA577","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c0e6b90c16ae5fa1eac19212a306cb84ffec72b","datavalue":{"value":{"entity-type":"item","numeric-id":5613969,"id":"Q5613969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$68AB43DD-0DF5-4DB1-8FED-46728137AA2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$CBD3E4C1-43AD-488B-9C44-C92F0D964F29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2167c65cce7cae937a43193ffcc320dfd4570b57","datavalue":{"value":{"entity-type":"item","numeric-id":5716582,"id":"Q5716582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$C86BF59C-328F-42D3-8D98-BBA5DB2434D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e242557b370e70ca22794bd752775ec0bac8856","datavalue":{"value":{"entity-type":"item","numeric-id":4804887,"id":"Q4804887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$423A6D3D-AD21-4DE2-901D-958BD3A58895","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11eefd7e7dc86c1755a8db4c6825e6e9fdeb6d39","datavalue":{"value":{"entity-type":"item","numeric-id":3619797,"id":"Q3619797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$35B50616-26F0-4E22-BE1B-DDB098F06253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae19a70a8616a64987bb08271f6f085e5255b8c5","datavalue":{"value":{"entity-type":"item","numeric-id":3908476,"id":"Q3908476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$05E83398-30B3-430E-ADCE-652C3F6BB449","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":"Q876046$8F0EA77A-EC8C-4BFD-86D6-573D178FD65E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d09db88e7db8de8a699f35dd014c509760be4233","datavalue":{"value":{"entity-type":"item","numeric-id":4157961,"id":"Q4157961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$10081D9A-D3DE-4CE7-AA3C-99216796990F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ff043886c15344e26a5762a58f1c95f9724f12c","datavalue":{"value":{"entity-type":"item","numeric-id":4594216,"id":"Q4594216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$09A9A040-3932-4AA4-BB0B-37FA52C4A5C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"afab4586824def7f2175c5532d1a1f9d233d0b27","datavalue":{"value":{"entity-type":"item","numeric-id":2723409,"id":"Q2723409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$D2F8694E-67A7-41DD-82D8-C16257704AB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"932383d1ac997ed208ef47dcb574b592efaf75b3","datavalue":{"value":{"entity-type":"item","numeric-id":4065031,"id":"Q4065031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$5FD53CCE-56A6-4B26-A25B-5D373B841AEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"394181bab27f4b1815f35966a93faec66f222ed4","datavalue":{"value":{"entity-type":"item","numeric-id":5703769,"id":"Q5703769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$4A53233A-9053-45CC-9932-A04F41D6824C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc90df82b5f45206962c7c11912a517a5a8f1843","datavalue":{"value":{"entity-type":"item","numeric-id":2848058,"id":"Q2848058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$B051BD8F-1BEB-4707-8B9D-A0DF531F0786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea96e16b6c447e5438826c7902ec9745c5df66e9","datavalue":{"value":{"entity-type":"item","numeric-id":2848059,"id":"Q2848059"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$3754096D-9843-4CAB-855F-BDA18B3050BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc3a61541eb0517ac7b63f9f303756a5a6805bca","datavalue":{"value":{"entity-type":"item","numeric-id":5703870,"id":"Q5703870"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q876046$72CA11C3-1541-4B04-909D-85680306FDD9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"03aa1ce2365c459c77186ff604cc2123f568ba52","datavalue":{"value":"10.1016/J.IC.2006.08.009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q876046$1E88B237-F66D-4EEE-962F-46BBC3875F88","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"003eb6e6a10d86419d74d48f76d4c083b7b6b731","datavalue":{"value":{"entity-type":"item","numeric-id":5703869,"id":"Q5703869"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee180785f5cc3f09ecde9bc6ca87196cf2332d82","datavalue":{"value":{"amount":"+0.9055677652359008","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":"Q876046$39B6E6C6-B336-4334-BA4B-7D2397903609","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56f33f58c88af48b5b15c4a3d931798c6b7c8bd6","datavalue":{"value":{"entity-type":"item","numeric-id":3408132,"id":"Q3408132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0f4df0692e9485184328bd67460a4655d76d420","datavalue":{"value":{"amount":"+0.8395673036575317","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":"Q876046$33A615EC-3627-4EF1-B398-8AF091B89AB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"533a8b77e8a99e85fa42a571379c69b8c18274f3","datavalue":{"value":{"entity-type":"item","numeric-id":1425161,"id":"Q1425161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"99d4c654cb828d87aff1bac8f783f8542812fe3a","datavalue":{"value":{"amount":"+0.8344461917877197","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":"Q876046$BFDBB359-C992-4B4B-AF9F-B09F0EDA008C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2956acbdbe54113a2ce780f06803ca8d04c1f41","datavalue":{"value":{"entity-type":"item","numeric-id":2723409,"id":"Q2723409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a50bedc02497e5d1792d8495af6e236ee8f5dc2","datavalue":{"value":{"amount":"+0.807460606098175","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":"Q876046$037E5488-CC19-42F1-83CF-A4389E2FB406","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bced0ca0afd16657834f724f6cddb80ceec6d421","datavalue":{"value":{"entity-type":"item","numeric-id":1730315,"id":"Q1730315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"013e8eb2d328b36b2d62ad4cdac2588767a3df75","datavalue":{"value":{"amount":"+0.7902466654777527","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":"Q876046$A8F3ACB3-0BEB-48B6-8C4F-776D3685F24F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Fast congruence closure and extensions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Fast_congruence_closure_and_extensions"}}}}}