resolution_rule (90B)
1 # Resolution rule 2 3 (C or x) AND (D or not x) IMPLIES C or D 4 5 Up: [satisfiability_boolean]