
(*TT* ((AND (OR (NOT |p2|) (NOT |p4|) |p3|)
            (OR (NOT |p3|) |p4| (NOT |p2|))
            (OR (NOT |p2|) (NOT |p3|) |p4|) (OR |p1| (NOT |p4|) |p2|)
            (OR (NOT |p3|) (NOT |p4|) (NOT |p2|))
            (OR (NOT |p3|) |p4| |p1|) (OR (NOT |p2|) (NOT |p3|) |p4|)
            (OR |p2| |p4| |p3|) (OR (NOT |p2|) |p1| |p3|)
            (OR (NOT |p2|) (NOT |p4|) (NOT |p1|))
            (OR (NOT |p3|) |p2| |p1|) (OR (NOT |p1|) |p3| |p4|)
            (OR |p1| (NOT |p3|) |p4|)
            (OR (NOT |p1|) (NOT |p3|) (NOT |p4|))
            (OR (NOT |p4|) (NOT |p2|) |p3|) (OR (NOT |p4|) |p3| |p1|)
            (OR |p2| (NOT |p3|) |p1|)
            (OR (NOT |p1|) (NOT |p3|) (NOT |p2|))
            (OR |p1| (NOT |p3|) (NOT |p2|))
            (OR (NOT |p3|) (NOT |p4|) |p2|)
            (OR |p1| (NOT |p4|) (NOT |p3|))
            (OR (NOT |p1|) |p3| (NOT |p2|)) (OR |p2| |p4| |p1|)
            (OR |p3| |p1| |p4|) (OR (NOT |p1|) |p2| (NOT |p3|))
            (OR |p2| |p4| |p1|) (OR |p1| |p4| (NOT |p2|))
            (OR |p1| |p4| (NOT |p2|)) (OR |p3| |p1| |p2|)
            (OR (NOT |p3|) (NOT |p1|) (NOT |p2|))
            (OR (NOT |p3|) (NOT |p4|) |p1|) (OR (NOT |p4|) |p3| |p2|)
            (OR (NOT |p1|) |p2| (NOT |p3|)) (OR |p4| (NOT |p2|) |p1|)
            (OR (NOT |p2|) |p4| (NOT |p1|))
            (OR (NOT |p4|) |p2| (NOT |p3|))
            (OR (NOT |p4|) |p1| (NOT |p3|))
            (OR (NOT |p2|) (NOT |p1|) |p4|) (OR |p2| (NOT |p4|) |p3|)
            (OR |p1| (NOT |p2|) |p4|))
       0.9038095))
(*TT* ((AND (OR |p4| |p1| (NOT |p3|))
            (OR (NOT |p1|) (NOT |p3|) (NOT |p4|))
            (OR (NOT |p3|) (NOT |p4|) |p2|)
            (OR (NOT |p4|) (NOT |p3|) |p1|)
            (OR (NOT |p2|) |p3| (NOT |p4|))
            (OR |p4| (NOT |p1|) (NOT |p2|)) (OR |p1| (NOT |p4|) |p2|)
            (OR |p4| (NOT |p3|) |p2|) (OR |p4| |p1| (NOT |p2|))
            (OR (NOT |p4|) |p3| (NOT |p2|)) (OR (NOT |p1|) |p3| |p4|)
            (OR |p2| (NOT |p1|) |p3|) (OR (NOT |p1|) |p2| |p3|)
            (OR (NOT |p4|) |p2| (NOT |p3|)) (OR |p1| (NOT |p4|) |p2|)
            (OR (NOT |p4|) (NOT |p3|) |p1|)
            (OR (NOT |p2|) (NOT |p1|) (NOT |p3|))
            (OR |p3| (NOT |p1|) (NOT |p2|)) (OR |p4| |p3| (NOT |p2|))
            (OR (NOT |p2|) |p3| (NOT |p4|))
            (OR (NOT |p4|) (NOT |p3|) (NOT |p2|))
            (OR (NOT |p4|) |p2| (NOT |p3|)) (OR (NOT |p2|) |p1| |p4|)
            (OR (NOT |p4|) |p3| (NOT |p2|))
            (OR |p2| (NOT |p3|) (NOT |p4|)) (OR (NOT |p1|) |p2| |p4|)
            (OR |p4| (NOT |p1|) |p3|) (OR |p2| (NOT |p1|) (NOT |p3|))
            (OR (NOT |p2|) |p3| |p4|) (OR (NOT |p3|) |p2| |p4|)
            (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))
            (OR |p1| (NOT |p3|) |p2|) (OR |p1| (NOT |p3|) (NOT |p2|))
            (OR |p2| (NOT |p3|) |p4|) (OR (NOT |p1|) (NOT |p3|) |p4|)
            (OR |p4| |p2| (NOT |p3|))
            (OR (NOT |p4|) (NOT |p2|) (NOT |p3|))
            (OR (NOT |p3|) |p1| |p2|) (OR (NOT |p2|) |p4| (NOT |p1|))
            (OR |p3| (NOT |p2|) (NOT |p1|)))
       0.323887))
(*TT* ((AND (OR |p4| (NOT |p2|) |p3|) (OR |p4| (NOT |p3|) (NOT |p2|))
            (OR |p3| (NOT |p2|) (NOT |p1|))
            (OR (NOT |p4|) (NOT |p2|) |p3|) (OR (NOT |p3|) |p4| |p2|)
            (OR (NOT |p4|) |p3| (NOT |p1|))
            (OR (NOT |p1|) (NOT |p2|) |p4|)
            (OR (NOT |p2|) |p4| (NOT |p3|))
            (OR (NOT |p4|) (NOT |p3|) |p2|)
            (OR |p4| (NOT |p2|) (NOT |p3|))
            (OR (NOT |p2|) (NOT |p3|) (NOT |p4|))
            (OR (NOT |p1|) (NOT |p3|) |p4|)
            (OR (NOT |p4|) |p2| (NOT |p3|)) (OR |p2| (NOT |p3|) |p4|)
            (OR (NOT |p1|) |p3| (NOT |p2|))
            (OR (NOT |p2|) (NOT |p1|) (NOT |p3|))
            (OR (NOT |p2|) |p4| (NOT |p3|))
            (OR (NOT |p4|) |p2| (NOT |p1|))
            (OR (NOT |p2|) |p3| (NOT |p1|))
            (OR (NOT |p2|) (NOT |p1|) |p3|)
            (OR (NOT |p4|) (NOT |p2|) |p3|)
            (OR (NOT |p2|) (NOT |p4|) |p3|) (OR (NOT |p4|) |p3| |p2|)
            (OR (NOT |p2|) |p3| |p1|) (OR (NOT |p1|) |p4| |p3|)
            (OR (NOT |p1|) |p4| |p3|)
            (OR (NOT |p2|) (NOT |p3|) (NOT |p4|))
            (OR (NOT |p2|) (NOT |p4|) |p1|) (OR (NOT |p2|) |p1| |p3|)
            (OR (NOT |p2|) (NOT |p4|) (NOT |p1|))
            (OR (NOT |p1|) |p2| |p4|)
            (OR (NOT |p4|) (NOT |p3|) (NOT |p1|))
            (OR |p3| (NOT |p4|) (NOT |p2|))
            (OR (NOT |p3|) (NOT |p1|) (NOT |p2|))
            (OR |p4| (NOT |p2|) |p1|) (OR |p1| (NOT |p3|) (NOT |p2|))
            (OR (NOT |p3|) |p1| (NOT |p2|))
            (OR (NOT |p1|) (NOT |p2|) |p3|) (OR |p4| (NOT |p2|) |p1|)
            (OR (NOT |p2|) (NOT |p1|) |p3|))
       0.3165851))
(*TT* ((AND (OR (NOT |p3|) (NOT |p2|) (NOT |p1|))
            (OR (NOT |p3|) (NOT |p1|) |p2|) (OR |p3| |p2| |p1|)
            (OR (NOT |p2|) |p4| (NOT |p3|))
            (OR (NOT |p1|) (NOT |p2|) |p3|)
            (OR (NOT |p1|) (NOT |p2|) |p4|)
            (OR (NOT |p2|) |p3| (NOT |p1|)) (OR |p3| (NOT |p2|) |p4|)
            (OR (NOT |p1|) |p4| |p3|) (OR (NOT |p2|) (NOT |p4|) |p1|)
            (OR (NOT |p3|) (NOT |p2|) |p1|) (OR |p3| (NOT |p1|) |p4|)
            (OR |p1| |p2| (NOT |p3|)) (OR |p1| |p4| (NOT |p3|))
            (OR (NOT |p3|) |p4| |p2|) (OR |p4| (NOT |p3|) (NOT |p1|))
            (OR (NOT |p2|) (NOT |p4|) |p1|) (OR |p1| (NOT |p4|) |p2|)
            (OR (NOT |p1|) (NOT |p3|) |p4|)
            (OR (NOT |p2|) |p1| (NOT |p4|))
            (OR (NOT |p1|) (NOT |p2|) (NOT |p3|))
            (OR (NOT |p1|) |p2| |p4|) (OR (NOT |p1|) |p4| |p2|)
            (OR (NOT |p3|) |p2| (NOT |p4|)) (OR |p3| (NOT |p2|) |p1|)
            (OR (NOT |p2|) |p1| (NOT |p4|)) (OR |p2| (NOT |p3|) |p1|)
            (OR |p3| |p2| (NOT |p4|)) (OR (NOT |p2|) |p3| |p1|)
            (OR (NOT |p4|) (NOT |p3|) |p1|) (OR (NOT |p3|) |p2| |p1|)
            (OR |p1| |p4| |p2|) (OR (NOT |p4|) (NOT |p3|) (NOT |p2|))
            (OR |p4| (NOT |p2|) (NOT |p1|)) (OR (NOT |p1|) |p3| |p4|)
            (OR (NOT |p2|) |p3| (NOT |p4|)) (OR (NOT |p3|) |p4| |p2|)
            (OR |p3| (NOT |p1|) |p4|) (OR (NOT |p4|) (NOT |p2|) |p1|)
            (OR |p3| |p1| (NOT |p4|)) (OR |p4| (NOT |p3|) |p2|)
            (OR |p1| |p2| (NOT |p4|)) (OR (NOT |p1|) |p2| (NOT |p3|))
            (OR (NOT |p3|) (NOT |p4|) (NOT |p1|)))
       0.653891))
(*TT* ((AND (OR (NOT |p3|) |p2| (NOT |p1|))
            (OR (NOT |p3|) (NOT |p1|) (NOT |p2|))
            (OR (NOT |p2|) |p3| (NOT |p1|))
            (OR (NOT |p4|) (NOT |p2|) (NOT |p1|))
            (OR |p4| (NOT |p1|) (NOT |p2|))
            (OR (NOT |p1|) (NOT |p3|) (NOT |p4|)) (OR |p3| |p1| |p2|)
            (OR (NOT |p4|) (NOT |p2|) |p3|) (OR |p3| (NOT |p4|) |p1|)
            (OR |p3| |p1| |p4|) (OR |p3| |p1| |p2|)
            (OR (NOT |p2|) (NOT |p1|) |p3|)
            (OR (NOT |p2|) (NOT |p4|) (NOT |p3|))
            (OR |p4| (NOT |p3|) |p2|) (OR (NOT |p4|) |p3| |p1|)
            (OR |p3| (NOT |p2|) (NOT |p1|)) (OR (NOT |p2|) |p3| |p1|)
            (OR (NOT |p2|) |p1| |p4|) (OR (NOT |p1|) |p3| (NOT |p4|))
            (OR (NOT |p4|) |p2| (NOT |p1|))
            (OR (NOT |p4|) (NOT |p1|) (NOT |p2|)) (OR |p4| |p3| |p2|)
            (OR (NOT |p1|) |p2| |p3|) (OR |p1| |p3| |p4|)
            (OR |p3| (NOT |p2|) (NOT |p4|))
            (OR (NOT |p1|) (NOT |p2|) (NOT |p4|))
            (OR |p2| (NOT |p3|) (NOT |p1|)) (OR |p4| (NOT |p3|) |p2|)
            (OR |p1| |p4| |p3|) (OR |p4| (NOT |p3|) (NOT |p2|))
            (OR (NOT |p1|) (NOT |p3|) |p2|) (OR (NOT |p3|) |p4| |p1|)
            (OR |p4| (NOT |p2|) (NOT |p1|)) (OR |p3| |p1| (NOT |p4|))
            (OR (NOT |p3|) |p4| |p2|) (OR (NOT |p2|) (NOT |p3|) |p4|)
            (OR |p2| |p1| |p4|) (OR |p1| (NOT |p2|) (NOT |p3|))
            (OR |p1| (NOT |p2|) |p3|) (OR |p2| |p4| |p3|)
            (OR (NOT |p3|) (NOT |p1|) (NOT |p4|))
            (OR (NOT |p1|) (NOT |p3|) (NOT |p2|))
            (OR |p1| (NOT |p2|) (NOT |p4|))
            (OR (NOT |p2|) |p4| (NOT |p3|)))
       0.6629578))
(*TT* ((AND (OR |p1| |p2| |p3|) (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))
            (OR |p3| (NOT |p4|) (NOT |p2|)) (OR |p4| (NOT |p3|) |p1|)
            (OR (NOT |p2|) |p3| |p1|) (OR |p1| |p4| |p3|)
            (OR (NOT |p2|) |p4| (NOT |p1|))
            (OR |p3| (NOT |p1|) (NOT |p4|)) (OR |p2| |p1| (NOT |p4|))
            (OR |p4| |p2| |p3|) (OR (NOT |p3|) (NOT |p4|) |p2|)
            (OR (NOT |p2|) |p4| |p3|) (OR |p1| (NOT |p4|) (NOT |p2|))
            (OR (NOT |p3|) |p4| |p1|) (OR |p2| |p4| (NOT |p1|))
            (OR (NOT |p4|) |p3| |p2|) (OR (NOT |p2|) |p1| |p4|)
            (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))
            (OR |p3| (NOT |p4|) |p1|) (OR |p2| (NOT |p1|) (NOT |p4|))
            (OR |p1| |p2| (NOT |p4|)) (OR (NOT |p3|) |p1| (NOT |p4|))
            (OR (NOT |p2|) |p4| (NOT |p3|))
            (OR |p2| (NOT |p3|) (NOT |p4|)) (OR |p4| (NOT |p2|) |p1|)
            (OR (NOT |p4|) |p1| |p3|) (OR |p3| (NOT |p1|) (NOT |p2|))
            (OR (NOT |p1|) |p3| |p4|) (OR |p3| (NOT |p1|) |p2|)
            (OR |p4| |p2| (NOT |p1|)) (OR |p3| |p2| (NOT |p4|))
            (OR |p1| |p3| (NOT |p4|)) (OR |p1| |p2| |p3|)
            (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))
            (OR |p2| (NOT |p1|) (NOT |p4|))
            (OR (NOT |p1|) (NOT |p2|) (NOT |p4|))
            (OR (NOT |p2|) |p4| |p1|) (OR |p2| |p4| |p1|)
            (OR (NOT |p4|) (NOT |p1|) (NOT |p2|))
            (OR |p3| (NOT |p1|) |p4|)
            (OR (NOT |p3|) (NOT |p2|) (NOT |p4|))
            (OR |p2| (NOT |p4|) |p1|) (OR |p4| (NOT |p1|) (NOT |p3|))
            (OR (NOT |p2|) (NOT |p3|) |p4|))
       0.0681705))
(*TT* ((AND (OR (NOT |p2|) |p3| (NOT |p1|))
            (OR (NOT |p4|) |p2| (NOT |p3|))
            (OR |p4| (NOT |p1|) (NOT |p2|)) (OR |p4| (NOT |p3|) |p1|)
            (OR |p1| |p3| (NOT |p2|)) (OR (NOT |p2|) |p3| |p1|)
            (OR |p2| (NOT |p3|) |p1|) (OR (NOT |p1|) |p4| |p3|)
            (OR (NOT |p4|) (NOT |p1|) (NOT |p3|))
            (OR (NOT |p3|) |p1| |p2|) (OR |p2| |p4| (NOT |p3|))
            (OR (NOT |p3|) |p2| |p1|) (OR |p1| |p3| (NOT |p4|))
            (OR (NOT |p4|) |p3| (NOT |p2|)) (OR |p1| |p3| |p4|)
            (OR |p1| (NOT |p4|) |p3|) (OR |p3| |p4| |p2|)
            (OR |p4| |p3| |p1|) (OR |p3| |p4| |p2|)
            (OR (NOT |p3|) (NOT |p2|) |p1|)
            (OR (NOT |p4|) |p2| (NOT |p3|)) (OR (NOT |p4|) |p3| |p1|)
            (OR (NOT |p3|) |p1| (NOT |p2|)) (OR |p2| (NOT |p4|) |p1|)
            (OR (NOT |p2|) |p1| |p4|) (OR |p3| |p2| |p4|)
            (OR |p1| |p4| (NOT |p3|)) (OR |p4| |p2| (NOT |p1|))
            (OR (NOT |p4|) (NOT |p2|) (NOT |p3|))
            (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))
            (OR (NOT |p3|) (NOT |p2|) (NOT |p1|))
            (OR (NOT |p2|) |p3| |p1|) (OR |p2| (NOT |p1|) |p4|)
            (OR |p3| |p4| (NOT |p2|)) (OR (NOT |p4|) (NOT |p1|) |p3|)
            (OR (NOT |p1|) |p2| |p3|)
            (OR (NOT |p3|) (NOT |p2|) (NOT |p1|))
            (OR |p3| (NOT |p1|) |p4|) (OR |p4| (NOT |p2|) (NOT |p3|))
            (OR |p1| |p4| |p2|) (OR |p2| |p4| (NOT |p3|))
            (OR (NOT |p3|) (NOT |p2|) (NOT |p1|))
            (OR (NOT |p1|) (NOT |p4|) (NOT |p3|))
            (OR |p2| (NOT |p3|) |p4|)
            (OR (NOT |p4|) (NOT |p1|) (NOT |p3|))
            (OR (NOT |p1|) (NOT |p4|) |p2|)
            (OR (NOT |p2|) (NOT |p4|) |p3|) (OR |p2| |p1| (NOT |p3|)))
       0.06914957))
(*TT* ((AND (OR |p2| (NOT |p3|) (NOT |p1|))
            (OR (NOT |p2|) (NOT |p3|) (NOT |p4|))
            (OR (NOT |p3|) |p4| (NOT |p2|))
            (OR (NOT |p1|) |p4| (NOT |p2|)) (OR (NOT |p3|) |p4| |p1|)
            (OR |p3| |p2| (NOT |p4|)) (OR |p3| |p1| |p4|)
            (OR (NOT |p1|) (NOT |p3|) |p2|)
            (OR (NOT |p3|) (NOT |p2|) |p1|) (OR |p1| |p4| (NOT |p2|))
            (OR |p1| (NOT |p2|) |p3|) (OR |p4| (NOT |p1|) (NOT |p2|))
            (OR (NOT |p2|) |p3| |p4|) (OR (NOT |p1|) |p4| (NOT |p2|))
            (OR |p2| |p4| (NOT |p3|)) (OR (NOT |p2|) |p3| (NOT |p4|))
            (OR (NOT |p1|) |p3| (NOT |p2|)) (OR (NOT |p3|) |p1| |p2|)
            (OR (NOT |p1|) (NOT |p4|) |p2|) (OR |p1| (NOT |p2|) |p3|)
            (OR |p2| (NOT |p1|) (NOT |p4|)) (OR (NOT |p1|) |p4| |p2|)
            (OR |p1| |p4| (NOT |p3|))
            (OR (NOT |p1|) (NOT |p4|) (NOT |p3|))
            (OR (NOT |p4|) |p3| |p1|)
            (OR (NOT |p3|) (NOT |p1|) (NOT |p2|))
            (OR (NOT |p2|) |p3| |p4|) (OR |p2| |p3| (NOT |p1|))
            (OR |p3| |p4| |p2|) (OR (NOT |p4|) (NOT |p1|) |p3|)
            (OR (NOT |p3|) |p4| |p1|) (OR |p4| (NOT |p1|) (NOT |p3|))
            (OR (NOT |p3|) (NOT |p4|) (NOT |p1|))
            (OR (NOT |p4|) |p3| |p2|)
            (OR (NOT |p3|) (NOT |p1|) (NOT |p2|))
            (OR |p3| (NOT |p2|) |p4|) (OR |p1| (NOT |p4|) (NOT |p2|))
            (OR |p1| |p2| |p4|) (OR |p1| (NOT |p3|) |p4|)
            (OR (NOT |p2|) (NOT |p4|) |p3|)
            (OR (NOT |p2|) |p3| (NOT |p1|))
            (OR (NOT |p4|) (NOT |p3|) (NOT |p2|))
            (OR (NOT |p3|) |p4| (NOT |p1|)) (OR |p3| |p2| (NOT |p1|))
            (OR (NOT |p3|) |p1| |p4|) (OR (NOT |p1|) (NOT |p2|) |p3|)
            (OR (NOT |p3|) |p4| |p1|) (OR |p3| (NOT |p4|) |p2|))
       0.7173184))
(*TT* ((AND (OR |p3| (NOT |p2|) (NOT |p4|))
            (OR (NOT |p4|) (NOT |p3|) (NOT |p1|))
            (OR |p2| (NOT |p3|) (NOT |p4|)) (OR |p3| (NOT |p4|) |p1|)
            (OR (NOT |p2|) (NOT |p4|) |p3|)
            (OR |p4| (NOT |p1|) (NOT |p2|))
            (OR (NOT |p1|) (NOT |p2|) |p3|)
            (OR (NOT |p1|) (NOT |p2|) |p3|)
            (OR |p3| (NOT |p4|) (NOT |p1|))
            (OR (NOT |p4|) (NOT |p1|) |p2|)
            (OR |p3| (NOT |p1|) (NOT |p4|))
            (OR (NOT |p4|) |p2| (NOT |p1|)) (OR |p4| |p1| |p2|)
            (OR (NOT |p3|) |p1| (NOT |p2|)) (OR (NOT |p4|) |p1| |p3|)
            (OR (NOT |p3|) (NOT |p2|) |p1|)
            (OR (NOT |p4|) |p2| (NOT |p3|)) (OR |p4| |p1| |p2|)
            (OR (NOT |p3|) |p4| |p2|)
            (OR (NOT |p1|) (NOT |p2|) (NOT |p4|))
            (OR (NOT |p1|) (NOT |p4|) (NOT |p2|))
            (OR |p1| (NOT |p3|) (NOT |p4|)) (OR |p3| (NOT |p2|) |p4|)
            (OR |p2| (NOT |p4|) |p3|) (OR |p3| (NOT |p4|) (NOT |p1|))
            (OR |p4| |p1| (NOT |p2|)) (OR |p3| (NOT |p1|) |p4|)
            (OR (NOT |p2|) |p3| |p4|) (OR (NOT |p3|) (NOT |p1|) |p4|)
            (OR (NOT |p3|) (NOT |p2|) |p4|)
            (OR |p1| (NOT |p4|) (NOT |p3|))
            (OR (NOT |p2|) (NOT |p4|) (NOT |p1|))
            (OR (NOT |p2|) |p4| |p3|) (OR |p4| |p3| (NOT |p1|))
            (OR (NOT |p2|) (NOT |p1|) (NOT |p3|))
            (OR (NOT |p3|) |p1| (NOT |p2|))
            (OR (NOT |p4|) (NOT |p2|) |p1|) (OR |p1| (NOT |p3|) |p4|)
            (OR |p4| (NOT |p1|) |p2|) (OR |p1| (NOT |p3|) (NOT |p4|))
            (OR |p2| (NOT |p1|) (NOT |p3|))
            (OR (NOT |p1|) (NOT |p4|) |p3|)
            (OR (NOT |p2|) (NOT |p1|) |p4|) (OR |p2| |p3| (NOT |p1|))
            (OR |p1| (NOT |p2|) (NOT |p3|)) (OR |p4| (NOT |p1|) |p3|)
            (OR |p3| |p1| (NOT |p2|))
            (OR (NOT |p1|) (NOT |p4|) (NOT |p2|)))
       0.6918694))