{"entities":{"Q6911405":{"pageid":20970448,"ns":120,"title":"Item:Q6911405","lastrevid":84159494,"modified":"2026-05-12T16:48:31Z","type":"item","id":"Q6911405","labels":{"en":{"language":"en","value":"SAT solving for variants of first-order subsumption"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8110395"}},"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":"Q6911405$1120C264-955C-4E58-A73C-C6ACE6F387DD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"216f697feb8e85b5506538b6de42c4cd23c433df","datavalue":{"value":{"text":"SAT solving for variants of first-order subsumption","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6911405$EDED31F2-3601-4B4E-9023-00C6B98A145C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3aa3e223c10e0bb7550626e0963ee4aa2d5267ed","datavalue":{"value":"10.1007/S10703-024-00454-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6911405$D595D80D-DCEE-42DC-8BB5-D3CC71B5D551","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"da4a0e9cbc7eb88d7f26443eed4f29f52cdc3984","datavalue":{"value":{"entity-type":"item","numeric-id":6492739,"id":"Q6492739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$7426E90C-E8E0-435F-B67E-5B680B3C4EE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ead90cf6f1840a157ecd158389beb38617898597","datavalue":{"value":{"entity-type":"item","numeric-id":2096453,"id":"Q2096453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$954240DA-F67E-4519-88DA-FB410C24A260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c317a0c80aecdbeefe69f1f6cac115022f894c88","datavalue":{"value":{"entity-type":"item","numeric-id":6429156,"id":"Q6429156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$D6B81652-0BF9-414F-B68C-5B792463B5F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"396db362b8f5a55e9aac7b42eacb07e40796d942","datavalue":{"value":{"entity-type":"item","numeric-id":209458,"id":"Q209458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$3094093D-4651-464C-A718-A247163AF1F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f17059e6c6c8a57972334867cc4d511b5d1368f5","datavalue":{"value":{"entity-type":"item","numeric-id":507357,"id":"Q507357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$B5144EC1-8400-4161-96BB-CFB3D9B88975","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"70551fcc6e89042fc26ae9242a005533b44a2d7a","datavalue":{"value":{"entity-type":"item","numeric-id":169908,"id":"Q169908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$594FC973-6793-46D6-9958-99D7BB06E16E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f508d3991dd2f46230f7c1046a08b37030d6343a","datavalue":{"value":{"time":"+2025-10-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6911405$6F622DF5-ED20-4C41-898F-1E860984D6C4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6911405$3B2FD872-37AB-4B98-BAC1-33740D1847D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7083a5d146d78edf9fc7469a5d9b0c104122f1b7","datavalue":{"value":"68R07","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6911405$0704BC7A-2F47-4646-9461-BB8FA7AE52F0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9dc97baa1cc5e7bff989ecde8138e33e4a862fb6","datavalue":{"value":"8110395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6911405$82A786F1-2402-4A1A-AA20-49B40BC089D6","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$AD968B93-F337-485D-8303-737088102276","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a313369d6da90dd1bef2143dee22ad776773a0ec","datavalue":{"value":"first-order theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6911405$2528D44B-C759-4CAE-82D8-85FA0D5FF117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87021f83c0bc2bfb13b38866d6825671687cfc77","datavalue":{"value":"SAT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q6911405$31D76DF6-40B6-4315-9D16-352DEA242DBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b6739fba16acf61162defd709061e3d3f6a05da4","datavalue":{"value":"saturation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6911405$59A290EF-114C-413A-B890-8FD434F5F940","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8c51344918cf160612586ae31930ddba9864b1c0","datavalue":{"value":"subsumption","type":"string"},"datatype":"string"},"type":"statement","id":"Q6911405$80F15CB5-7E8E-4B2B-B6C9-677B90F6DBE6","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":"Q6911405$C6752B52-6214-4E68-87BB-893C2D764568","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f1060c39f6c78c6c906f6922c72b026efa0999e0","datavalue":{"value":{"entity-type":"item","numeric-id":518396,"id":"Q518396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$7F172754-D725-4358-AC99-58F66D28A174","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8209e2641ba17dd4f4c7ce79db79a957c2e8bd37","datavalue":{"value":{"entity-type":"item","numeric-id":6535528,"id":"Q6535528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$A1746C5C-2E45-4055-8DDF-383C8A5E8E17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fac4b7778485439dbda9e84cba0eb78fe846df5b","datavalue":{"value":{"entity-type":"item","numeric-id":6091296,"id":"Q6091296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$FF3A3D31-4FAB-4AF9-83CF-819AFBE1D4AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9370899dedc1d653d16f1f5aaa8b6c6be96f529c","datavalue":{"value":{"entity-type":"item","numeric-id":3604000,"id":"Q3604000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$8C64EE07-8289-4E92-9FBD-EEC1695C31F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86c32d3283dbc1fe39bfc7c16048659fcd75d91f","datavalue":{"value":{"entity-type":"item","numeric-id":1687553,"id":"Q1687553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$1D7C1F63-DACC-48FD-8E7F-9C4FCB3BA68E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48933c0d362727730cc1905c68ff87e3a22216cf","datavalue":{"value":{"entity-type":"item","numeric-id":2457345,"id":"Q2457345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$10EBF9CC-9D80-40F2-889B-5FAC17532F41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f14878b4342799995051ac9bc54cd21c98efc98","datavalue":{"value":{"entity-type":"item","numeric-id":2751359,"id":"Q2751359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$8D360C1A-B88D-483A-A6F4-E104DAF1F262","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":"Q6911405$0E756DDC-E664-4D6B-B967-00C17DA77264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aefe5e0f2b827afb25f0a8067d25c4a893f91ca","datavalue":{"value":{"entity-type":"item","numeric-id":4304492,"id":"Q4304492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$D325B7DC-6FE4-4639-AAB5-82865C8B9457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bda68c490d3eacdbb4c205fd2cca76126f0a9248","datavalue":{"value":{"entity-type":"item","numeric-id":5714773,"id":"Q5714773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$5C47FA65-C11A-49BA-939E-60E60A680D9B","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":"Q6911405$E356D1AE-B17A-4BCD-9704-B101ADC272AF","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":"Q6911405$9789E149-695E-4DCE-9366-19FBF9399FA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ce5dec0979ee80b250e5f4d24210da01a00ee71d","datavalue":{"value":{"entity-type":"item","numeric-id":4913860,"id":"Q4913860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$A7A6400A-ED04-46F1-918B-B66CA6ECF615","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c32eeb969eda472fde77b77bf83c3f4e02690290","datavalue":{"value":{"entity-type":"item","numeric-id":3785940,"id":"Q3785940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$41B88921-EA28-4103-AA40-58ADB5DA6E28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aee320825812c934cb06541d86c0004e860fe7ce","datavalue":{"value":{"entity-type":"item","numeric-id":6492740,"id":"Q6492740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$4FC90DEC-0980-4D7A-9F0A-51A237061E27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c47996ece75ce993dce6ae30ef206590df431f6","datavalue":{"value":{"entity-type":"item","numeric-id":2096454,"id":"Q2096454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$88011BA6-54C3-47F4-9596-97F128DCA567","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e25c5c645463d02bb7c5993e3929114f96a3491","datavalue":{"value":{"entity-type":"item","numeric-id":6643075,"id":"Q6643075"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$AF6D45E7-A847-4C31-AEEC-B0C76260C33C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bfa160377609209cc0086df75c8fab81fffcf5cc","datavalue":{"value":{"entity-type":"item","numeric-id":6056639,"id":"Q6056639"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$7D6B7231-B1D1-4960-BC28-33A8D2AEA9F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4aa6750f3149d248c4e232f6fdbdc36d7bc86e39","datavalue":{"value":{"entity-type":"item","numeric-id":2920991,"id":"Q2920991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$6FBC6901-3F88-4396-A34E-032D7E917136","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":"Q6911405$44215604-53AB-418D-81D1-DC2B1A935FF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cdbfb47549943b1416c0ea31be53503a2cffb8d0","datavalue":{"value":{"entity-type":"item","numeric-id":5396710,"id":"Q5396710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$1A9D4219-B6EE-4B09-96FC-ACDE298E55A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba0262656e41c382f9f5a9a7b3bb892ab61ed599","datavalue":{"value":{"entity-type":"item","numeric-id":5270493,"id":"Q5270493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$AA62514C-8FDE-4AA4-8386-E8F9A24D11E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"916f90652d55a7043c8bb9e5cf36216cc37b0d7f","datavalue":{"value":{"entity-type":"item","numeric-id":3771609,"id":"Q3771609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$4E90EC01-6477-4B5B-9408-201051F25454","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a3bc28bbd3ceb63e1371d2c218ba029bf15797f","datavalue":{"value":{"entity-type":"item","numeric-id":3716319,"id":"Q3716319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$D8132329-0C73-4AAC-92E5-FC3378DFD5A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db01f3c17780383599ab48b43f14b3b48d73b1e5","datavalue":{"value":{"entity-type":"item","numeric-id":4649734,"id":"Q4649734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$B635A9C8-DE18-4F4D-A26A-18A8C4A42618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ecf772690cf31a35a32c2f2f4f39692662f8aa11","datavalue":{"value":{"entity-type":"item","numeric-id":2303251,"id":"Q2303251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$985F0A41-8D49-4384-A483-27214167AEEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22ef5f661c4f0016c7fdb92e88e8b94907f8385b","datavalue":{"value":{"entity-type":"item","numeric-id":5713748,"id":"Q5713748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6911405$C11D6CCC-A4E2-4813-A148-1CFE90CE0DCE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"SAT solving for variants of first-order subsumption","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/SAT_solving_for_variants_of_first-order_subsumption"}}}}}