Statistics: sg: 2 nodes, 1 edge, 1 class, 0 constraints cg slice: 26 nodes, 46 edges Strategy graph: { Formula -> * } source:Formula source-edge:0 target:* Class graph slice: LiteralCons = Literal LiteralList extends LiteralList. SatAbsent = extends SatOpt. ClauseEmpty = extends ClauseList. UnsatClause = extends Clause. Literals : SatLiteral | UnsatLiteral | LiteralList . ClauseList : ClauseCons | ClauseEmpty . Clause : SatClause | UnsatClause | ConcreteClause . SatLiteral = extends Literals. Weight = Integer . SatCount = Integer extends SatOpt. LiteralEmpty = extends LiteralList. UnsatAbsent = extends UnsatOpt. SatOpt : SatCount | SatAbsent . ClauseCons = Clause ClauseList extends ClauseList. Positive = extends Literal. Formula = ClauseList SatOpt UnsatOpt . UnsatCount = Integer extends UnsatOpt. SatClause = extends Clause. ConcreteClause = Weight Literals extends Clause. Variable = Integer . Negative = extends Literal. LiteralList : LiteralCons | LiteralEmpty extends Literals. UnsatLiteral = extends Literals. Literal : Positive | Negative common Variable . UnsatOpt : UnsatCount | UnsatAbsent .