Statistics: sg: 2 nodes, 1 edge, 1 class, 0 constraints cg slice: 17 nodes, 23 edges Strategy graph: { Formula -> * } source:Formula source-edge:0 target:* Class graph slice: Negative = extends Literal. Variable = Ident . Positive = extends Literal. Literal_List = Nonempty_Literal_List . Literal : Positive | Negative common Variable . Unsatisfied = extends Body. Nonempty_Clause_List = Clause [ Nonempty_Clause_List ] . Formula = Clause_List . Satisfied = extends Body. Nonempty_Literal_List = Literal [ Nonempty_Literal_List ] . Weight = float . Clause = Weight Body . Literals = Literal_List extends Body. Body : Satisfied | Unsatisfied | Literals . Clause_List = Nonempty_Clause_List .