
(*ISC* |a1|
       (AND (OR (NOT (ALL |r1| (OR (NOT |p5|) (NOT |p2|) |p9|)))
                (ALL |r1| (OR |p5| |p7| |p8|))
                (ALL |r1| (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))))
            (OR (ALL |r1| (OR |p8| |p7| |p10|))
                (ALL |r1| (OR |p7| (NOT |p4|) |p9|))
                (ALL |r1| (OR |p4| |p10| |p2|)))
            (OR (ALL |r1| (OR |p9| (NOT |p5|) |p8|))
                (ALL |r1| (OR (NOT |p1|) (NOT |p4|) |p6|))
                (NOT (ALL |r1| (OR (NOT |p3|) (NOT |p4|) (NOT |p9|)))))
            (OR (NOT (ALL |r1| (OR |p9| (NOT |p10|) |p1|)))
                (ALL |r1| (OR |p1| (NOT |p8|) |p3|))
                (ALL |r1| (OR |p3| |p8| (NOT |p9|))))))
(*ISC* |a1|
       (AND (OR (NOT (ALL |r1| (OR (NOT |p4|) |p7| |p6|)))
                (ALL |r1| (OR |p6| (NOT |p3|) |p9|))
                (ALL |r1| (OR |p1| (NOT |p9|) |p6|)))
            (OR (ALL |r1| (OR (NOT |p2|) |p3| (NOT |p4|)))
                (ALL |r1| (OR (NOT |p1|) (NOT |p7|) |p2|))
                (ALL |r1| (OR (NOT |p3|) |p9| |p5|)))
            (OR (ALL |r1| (OR (NOT |p5|) (NOT |p9|) (NOT |p10|)))
                (NOT (ALL |r1| (OR |p1| |p3| |p5|)))
                (NOT (ALL |r1| (OR |p7| |p1| (NOT |p2|)))))
            (OR (NOT (ALL |r1| (OR |p10| (NOT |p1|) |p5|)))
                (NOT (ALL |r1| (OR |p6| |p1| |p7|)))
                (NOT (ALL |r1| (OR |p8| |p6| |p1|))))))
(*ISR* (|a4| |a3|) |r1|)
(*ISR* (|a4| |a1|) |r1|)