{"entities":{"Q5881799":{"pageid":7911350,"ns":120,"title":"Item:Q5881799","lastrevid":97560428,"modified":"2026-06-05T15:00:44Z","type":"item","id":"Q5881799","labels":{"en":{"language":"en","value":"Characterizing Tseitin-Formulas with Short Regular Resolution Refutations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7662468"}},"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":"Q5881799$A5D97AE0-BED3-4EFD-80C2-9D80457FE469","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ac7dd7ec8d2ae852909d6f2dae280d4ce65660d5","datavalue":{"value":{"text":"Characterizing Tseitin-Formulas with Short Regular Resolution Refutations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5881799$4A4D971A-CE8E-4E30-9084-4D3357C8D5B9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b2ac30df409f8849a3a2808219556f916f3d9b39","datavalue":{"value":"1506.68062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$C7D39010-CB95-489C-AD43-53EFE33834C5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb8d8c9f8c88a0cf010eabd9eb58e7a111d99f1d","datavalue":{"value":{"entity-type":"item","numeric-id":2118290,"id":"Q2118290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$E115C36D-C2E0-4F3C-9915-F4B10DA9B5F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"39a64a952a06abada0a21aa13e218a56ddab0066","datavalue":{"value":{"entity-type":"item","numeric-id":269341,"id":"Q269341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$563D0895-4C4D-4CF2-BB69-4C34492DA627","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"bb469f8c3341c58b96368431d3c87cbee3d3281e","datavalue":{"value":{"entity-type":"item","numeric-id":110835,"id":"Q110835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$1A97EF6A-80B2-46FD-A722-17091991A334","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"89caa31fd22a360d487b4d2ba44c1d87259c2aff","datavalue":{"value":{"time":"+2023-03-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":"Q5881799$8BABAB29-6B00-4E3A-9717-EF3323A9FEB5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$14E65E92-68C5-48A1-A3B9-7729A05F2187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ece9b879f80d96e2a1d45b28bdcc8cfa6b01861e","datavalue":{"value":"03F20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$540F0D60-A19C-4791-8FA3-FBDCFFD4CE78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"344f62a15ccd40e690364bd758985e8313f47f4a","datavalue":{"value":"68R10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$82B6ED55-D5AD-4FA2-97F1-B60B82D2C155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$B5A34233-4847-4528-B081-4D78E8A9481C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b0ed6c9f5350823011d31c07169b4964f6cbb76d","datavalue":{"value":"7662468","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$8ECF9AD6-E66D-43D5-985E-2A2EC3FD199C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"252f9f9ed9fe8ca406cc19fba38a46c0414791ee","datavalue":{"value":"satisfiability","type":"string"},"datatype":"string"},"type":"statement","id":"Q5881799$05C04BBA-372E-4CC0-A7C0-0B088BE55C94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe99cc33cb0d5ac2e6c3a73729bf23aa7caccf7b","datavalue":{"value":"knowledge representation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5881799$4CE7C107-4D47-4A78-A903-27C4316AABEB","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":"Q5881799$4EBBA0C8-4E38-4FA9-A094-200CE9CFCC45","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d2f759e6833df0050e1b693d236025562e6c42fb","datavalue":{"value":"https://doi.org/10.1613/jair.1.13521","type":"string"},"datatype":"url"},"type":"statement","id":"Q5881799$2AE67F1B-4D7F-4239-B548-26DA36C8A688","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c8cc6428ee7295b2784be8ce8c58afb0f7965056","datavalue":{"value":"W3136246162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$54AC654E-2D8B-4F2F-A4F0-60CEBBB6B3C8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"25eb460d58931676e51733807df783912964924b","datavalue":{"value":{"entity-type":"item","numeric-id":3002781,"id":"Q3002781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$4E4D485E-0E54-4493-A5ED-20EE8DB37C6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e8e50187a51221a00e96148d3b4590c3646576b","datavalue":{"value":{"entity-type":"item","numeric-id":430830,"id":"Q430830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$41BC24F8-DC1C-4035-BAD4-3CB7F4EF9FC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f8b49fb1213506b170f8db77c1d65bdba91599f","datavalue":{"value":{"entity-type":"item","numeric-id":778533,"id":"Q778533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$965A5C7B-D39C-446E-A828-EE4F510E72FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70335fcaeda9b5ca37e671e8ec490e405b6976d3","datavalue":{"value":{"entity-type":"item","numeric-id":5230344,"id":"Q5230344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$E40D336D-5D53-4AED-B6AB-95F0C11BA0BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7620e2916af53d435ea4ff922a32c34908193ede","datavalue":{"value":{"entity-type":"item","numeric-id":5415477,"id":"Q5415477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$06C8941C-F338-4084-9713-0B32CFF8DD5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82879da4a42c15f2d8963e9ae87cc161e327d5d5","datavalue":{"value":{"entity-type":"item","numeric-id":5495819,"id":"Q5495819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$7B02C737-25C3-4B7D-8DA7-7AF5B31C70F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5865ff2d33453d31523070266b6906b7f0fdaee0","datavalue":{"value":{"entity-type":"item","numeric-id":1430570,"id":"Q1430570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$7A161A0D-D5A1-41A4-AF99-A70771E6AA3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7033f613f87271bbae4d15c33caa982a0486ba8","datavalue":{"value":{"entity-type":"item","numeric-id":819825,"id":"Q819825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$1E396E54-F2A9-46E3-B7FA-9E3D18860E7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98b011ab831949ce741780553369025dd5b73c2d","datavalue":{"value":{"entity-type":"item","numeric-id":5148371,"id":"Q5148371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$2B2FA3E1-6F4D-4E41-80B0-69411D805E87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6058e41538d30b2785f508777500d056457628f","datavalue":{"value":{"entity-type":"item","numeric-id":5441353,"id":"Q5441353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$2D3E3CD1-D937-43A8-9C2A-4412E7C68EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74710e9d2e1ae04d62da8162f48ee143c6479921","datavalue":{"value":{"entity-type":"item","numeric-id":4411139,"id":"Q4411139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$37B5CB68-A336-413E-9313-73287E4B6EB1","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":"Q5881799$6F511F53-8D4D-418C-A3B5-0704CCB2EF7C","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":"Q5881799$50995197-FEBF-4692-9DA6-CD114DB8B3C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fee8fb57a07f9ec7b39019dc31145cee63c491f8","datavalue":{"value":{"entity-type":"item","numeric-id":5092411,"id":"Q5092411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$D13BF7E3-49FB-4E3F-AD9B-B8E10290AFA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2c11f9d66aafa941398d90496eed7436ea3694f","datavalue":{"value":{"entity-type":"item","numeric-id":5053060,"id":"Q5053060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$9ABEFBBE-2374-4EE5-A7E9-8CE93FD23A99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8208fd73ae310ac25c442151ea4993bdac39020f","datavalue":{"value":{"entity-type":"item","numeric-id":5111240,"id":"Q5111240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$08E31320-968B-4CCE-83C4-A337A16C864F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88395289f23572a36bd4c54ae7a90e6673a30fdc","datavalue":{"value":{"entity-type":"item","numeric-id":3137703,"id":"Q3137703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$CF3D80CE-FF19-4217-9E33-C1CDD1ED4329","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5dc42a680b8ef6292b67bd3175f40575a5cbf46","datavalue":{"value":{"entity-type":"item","numeric-id":2978180,"id":"Q2978180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$5708107D-4543-4AC8-A152-46AB8C689C85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"046817c7ca080b41f58e0fe1b44cba8f32931536","datavalue":{"value":{"entity-type":"item","numeric-id":4928481,"id":"Q4928481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$402AA0A9-6D71-4A1B-B35B-9CD77A959258","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64aeb75c0c62d59211d5133f95345827288a0e73","datavalue":{"value":{"entity-type":"item","numeric-id":1983330,"id":"Q1983330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$5EA52C74-E6BE-4D25-84F0-4A03ACD265A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa34ae3e34f6a863a9f8db67c2bfb8bb6401943","datavalue":{"value":{"entity-type":"item","numeric-id":4856172,"id":"Q4856172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$C9014D2D-A60B-48E2-8270-F24DFDCCC228","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80f94c357cde2b4f18340db99582ef961b69ec90","datavalue":{"value":{"entity-type":"item","numeric-id":309788,"id":"Q309788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$DBDD0F5F-6B43-43E7-9A58-15B6D47D2A77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36bf65b673444e6f5fc6bfae60c9a140bab18719","datavalue":{"value":{"entity-type":"item","numeric-id":4734768,"id":"Q4734768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$ABAF9B75-25AF-4027-A248-47DAA62278B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c6b871d25a3f2bcc10ef5d12d2a6df59054c7c5","datavalue":{"value":{"entity-type":"item","numeric-id":5604434,"id":"Q5604434"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$B5E2ED40-C555-46A3-B067-DFC79982F19A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"728810277830424bd131e6e77eef399df584ccea","datavalue":{"value":{"entity-type":"item","numeric-id":3780485,"id":"Q3780485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$DDF74C4E-B5B9-4754-A2FB-0B753827FE75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"509c8c073466afc7f6722bfaf6f12fb08af4e849","datavalue":{"value":{"entity-type":"item","numeric-id":2999857,"id":"Q2999857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$1AA16BD0-A320-45CD-8F76-B509E864A57D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"498da7736cddcc92e38f3ffffc1b5b5d81e5aa53","datavalue":{"value":{"entity-type":"item","numeric-id":2661346,"id":"Q2661346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5881799$8FF842A1-6B88-4F2D-B5B0-1E80B25E4B37","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"eba5954cfe22cd859069673669f9f1420b06448c","datavalue":{"value":"10.1613/JAIR.1.13521","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5881799$4E8A2DC3-1B1B-4478-80A2-4B8AD67F321F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8361b86ea858c692159e5238a9f0fe78f3c9e3b2","datavalue":{"value":{"entity-type":"item","numeric-id":1983330,"id":"Q1983330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a736093a30f78c0f0baa0bc3f9de52f7fa30e3a0","datavalue":{"value":{"amount":"+0.8953409194946289","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":"Q5881799$DEBA4169-7936-4765-9A4F-97DDCB4E0EC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2d29bbf1bbc9f5aba33489e7969f75d6c388d7e","datavalue":{"value":{"entity-type":"item","numeric-id":2894482,"id":"Q2894482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eeaf2612373a7b9becef514dfc18262ec75dbaa2","datavalue":{"value":{"amount":"+0.855021059513092","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":"Q5881799$4E611F08-481B-43AF-B065-AC2AAE45828B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf0e719f92396c6fcced37aa6f2e597b63afe986","datavalue":{"value":{"entity-type":"item","numeric-id":2084956,"id":"Q2084956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"26a00a5034c930d0f61b9f4eb99af20166299cf2","datavalue":{"value":{"amount":"+0.8300251364707947","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":"Q5881799$31AD4395-B8CF-42F3-B402-B36C15DE7451","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0446609fbf51d84f72179960efae06213341b5d1","datavalue":{"value":{"entity-type":"item","numeric-id":2330557,"id":"Q2330557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd3f2d353e89fae689e851ed63bea99e4df77fb7","datavalue":{"value":{"amount":"+0.8189958333969116","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":"Q5881799$F5341ADD-4615-4A9F-8535-DCF8F11965D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"647d633f4bac67deaa804e390e32723ea06b684a","datavalue":{"value":{"entity-type":"item","numeric-id":4036560,"id":"Q4036560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8584112dddd0de25b865c1c4b94fa487e0239970","datavalue":{"value":{"amount":"+0.7941319346427917","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":"Q5881799$E78AD147-1088-4032-A1D3-CEACA39936FD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Characterizing Tseitin-Formulas with Short Regular Resolution Refutations","badges":[]}}}}}