ในทางตรรกศาสตร์ การเขียนข้อสรุป C จากข้อสมมติ A นั้นจะถูกต้องถ้าประโยค   นั้นเป็นสัจนิรันดร์ (หรือในอีกทางหนึ่งก็คือ ในทุก ๆ กรณีที่ A เป็นจริง C จะต้องเป็นจริงด้วย)

คุณได้รับข้อสรุปและข้อสมมติมาหลายชุด จงเขียนโปรแกรมเพื่อตรวจสอบว่าข้อสรุปดังกล่าวนั้น ถูกต้องตามข้อสมมติหรือไม่?

เราจะใช้ตัวอักษรตั้งแต่ a ถึง p (รวม 16 ตัว) แทนประพจน์ใด ๆ   สำหรับการระบุข้อสมมติและข้อสรุปเราจะระบุด้วยวิธีการเขียนแบบ Conjunctive Normal Form นั่นคือ  เราจะระบุนิพจน์ทางตรรกศาสตร์ในรูปของตัวดำเนินการ AND กันของนิพจน์ที่ประกอบด้วยตัวแปรที่ OR กัน  ตัวอย่างเช่น   (a v b v ~c) ^ (c v ~d) ^ (d v ~a) เป็นการ AND กันของสามนิพจน์คือ    (a v b v ~c) , (c v ~d) และ   (d v ~a) เราสังเกตได้ว่าแต่ละนิพจน์จะมีตัวดำเนินการ OR กันของประพจน์ภายใน เราขอเรียกนิพจน์นี้ว่า clause   ในการเขียนนิพจน์ดังกล่าวข้างต้นในข้อมูลนำเข้าเราจะเขียนแยกเป็นสามบรรทัด บรรทัดละ clause ดังนี้

3 +a +b –c    (a v b v ~c)
2 +c –d      (c v ~d)
2 +d –a    (d v ~a)

โดยในแต่ละบรรทัดจะขึ้นด้วยจำนวนเต็ม c แทนจำนวนตัวแปรใน clause นั้น  (1 <= c <= 32) ตามด้วยสายอักขระความยาวสองตัวอักขระอีก c สาย โดยแต่ละสายอักขระคั่นด้วยช่องว่างหนึ่งช่อง ทั้งนี้สายอักขระความยาวสองแต่ละสายอักขระจะขึ้นด้วยอักขระ + หรือ – โดย จะเป็นการระบุว่าตัวแปรที่ตามมานั้นไม่ใส่ หรือใส่ ตัวดำเนินการ NOT (~)  อักขระถัดมาจะแทนตัวแปร

ข้อมูลนำเข้า
บรรทัดแรกมีจำนวนเต็ม k แทนจำนวนข้อมูลชุดทดสอบย่อย (1 <= k <= 3)  จากนั้นข้อมูลจะประกอบด้วยข้อมูลชุดทดสอบย่อย จำนวน k ชุด เรียงกันไป   ข้อมูลชุดทดสอบย่อยแต่ละชุดจะไม่เกี่ยวข้องกัน
บรรทัดแรกของแต่ละข้อมูลชุดทดสอบย่อยมีจำนวนเต็ม n และ m แทนจำนวน clause ของข้อสมมติ และจำนวน clause ของข้อสรุปตามลำดับ (1<= n <= 100; 1 <= m <= 100) 
จากนั้น บรรทัดที่ 2 ถึงบรรทัดที่ 1 + n ในข้อมูลชุดทดสอบย่อยนี้จะแสดงแต่ละ clause ของข้อสมมติ   และบรรทัดที่ 2+n ถึง 1+n+m ของข้อมูลชุดทดสอบย่อยจะระบุแต่ละ clause ของข้อสรุป ในรูปแบบเดียวกัน

ข้อมูลส่งออก
มีทั้งสิ้น k บรรทัด โดยในบรรทัดที่ i จะมีข้อความว่า YES ถ้าข้อสรุปของข้อมูลชุดทดสอบย่อยที่ i ถูกต้องตามข้อสมมติ  และจะมีข้อความว่า NO ถ้าไม่ถูกต้อง

ที่มา: สอบปฏิบัติ ครั้งที่ 1 ค่ายคัดเลือกผู้แทนประเทศไทย ไปแข่งขันคอมพิวเตอร์โอลิมปิกระหว่างประเทศ ปี 2550 ค่ายที่ 1

คำอธิบายตัวอย่างข้อมูลนำเข้า
ข้อมูลชุดทดสอบย่อยแรก
ข้อสมมติ:  (~a v b) ^ (~b v c) ^ (~c)
ข้อสรุป:  ~a (ถูกต้อง)
ข้อมูลชุดทดสอบย่อยที่สอง
ข้อสมมติ:  b
ข้อสรุป:  ~a    (ไม่ถูกต้อง)