
(*NT* (AND (OR (NOT |p2|) (NOT |p3|) (NOT |p1|))
           (OR |p6| (NOT |p5|) (NOT |p4|))))
(*NT* (AND (OR |p4| |p5| |p1|) (OR (NOT |p5|) (NOT |p1|) (NOT |p2|))))
(*NT* (AND (OR (NOT |p3|) |p6| |p5|) (OR |p4| |p6| |p5|)))
(*NT* (AND (OR |p1| (NOT |p4|) |p3|) (OR (NOT |p4|) |p5| |p3|)))
(*NT* (AND (OR |p6| (NOT |p2|) (NOT |p5|)) (OR |p4| |p5| (NOT |p3|))))
(*NT* (AND (OR |p5| (NOT |p6|) (NOT |p3|))
           (OR (NOT |p3|) |p4| (NOT |p6|))))
(*NT* (AND (OR (NOT |p1|) (NOT |p6|) (NOT |p5|)) (OR |p2| |p5| |p1|)))
(*NT* (AND (OR (NOT |p2|) (NOT |p3|) |p6|)
           (OR (NOT |p3|) (NOT |p5|) |p2|)))
(*NT* (AND (OR |p5| (NOT |p6|) |p1|) (OR (NOT |p2|) (NOT |p1|) |p5|)
           (OR |p4| (NOT |p5|) (NOT |p2|)) (OR |p6| |p2| |p1|)))
(*NT* (AND (OR (NOT |p6|) |p4| |p2|)
           (OR (NOT |p5|) (NOT |p2|) (NOT |p6|))
           (OR |p2| |p5| (NOT |p1|)) (OR (NOT |p4|) |p1| |p5|)))
(*NT* (AND (OR (NOT |p2|) |p6| |p3|) (OR |p1| (NOT |p2|) (NOT |p5|))
           (OR (NOT |p6|) |p5| |p1|) (OR |p2| |p3| (NOT |p6|))))
(*NT* (AND (OR |p4| (NOT |p6|) (NOT |p5|)) (OR |p3| |p2| |p6|)
           (OR (NOT |p1|) |p3| (NOT |p2|)) (OR |p3| |p6| |p1|)))
(*NT* (AND (OR |p4| (NOT |p3|) |p5|) (OR |p4| |p1| |p3|)
           (OR |p2| |p4| |p3|) (OR (NOT |p2|) (NOT |p4|) |p6|)))
(*NT* (AND (OR (NOT |p1|) (NOT |p4|) (NOT |p6|)) (OR |p6| |p1| |p3|)
           (OR (NOT |p5|) (NOT |p6|) |p3|)
           (OR (NOT |p6|) (NOT |p4|) |p2|)))
(*NT* (AND (OR |p3| (NOT |p4|) (NOT |p2|)) (OR (NOT |p1|) |p6| |p5|)
           (OR |p5| (NOT |p6|) |p1|) (OR (NOT |p6|) |p2| |p1|)))
(*NT* (AND (OR (NOT |p2|) (NOT |p6|) |p1|)
           (OR (NOT |p2|) (NOT |p6|) |p4|) (OR (NOT |p4|) |p6| |p5|)
           (OR (NOT |p3|) (NOT |p2|) (NOT |p4|))))
(*NT* (AND (OR |p5| |p2| |p4|) (OR |p3| (NOT |p2|) (NOT |p4|))
           (OR |p6| |p1| (NOT |p3|)) (OR (NOT |p4|) |p6| |p3|)
           (OR |p5| (NOT |p6|) (NOT |p3|))
           (OR (NOT |p6|) |p4| (NOT |p2|))))
(*NT* (AND (OR |p2| (NOT |p1|) (NOT |p4|))
           (OR |p2| (NOT |p3|) (NOT |p5|)) (OR |p3| |p4| (NOT |p6|))
           (OR |p4| |p1| (NOT |p6|)) (OR |p3| |p2| (NOT |p6|))
           (OR (NOT |p6|) |p3| |p5|)))
(*NT* (AND (OR |p1| |p4| (NOT |p5|)) (OR |p4| (NOT |p1|) |p2|)
           (OR (NOT |p1|) (NOT |p4|) |p5|)
           (OR (NOT |p3|) |p2| (NOT |p4|))
           (OR (NOT |p2|) (NOT |p5|) (NOT |p6|))
           (OR |p3| |p2| (NOT |p6|))))
(*NT* (AND (OR (NOT |p2|) (NOT |p5|) (NOT |p1|))
           (OR |p5| (NOT |p3|) |p2|) (OR |p6| |p1| |p4|)
           (OR |p1| |p2| (NOT |p6|)) (OR (NOT |p1|) |p3| (NOT |p2|))
           (OR (NOT |p4|) |p2| |p6|)))
(*NT* (AND (OR |p2| |p1| |p6|) (OR (NOT |p3|) |p2| |p6|)
           (OR (NOT |p5|) |p2| (NOT |p3|)) (OR |p4| |p1| |p2|)
           (OR (NOT |p4|) (NOT |p1|) (NOT |p2|))
           (OR (NOT |p5|) (NOT |p6|) (NOT |p4|))))
(*NT* (AND (OR |p5| |p3| |p6|) (OR |p6| |p3| (NOT |p1|))
           (OR |p3| (NOT |p4|) |p6|) (OR (NOT |p3|) |p1| (NOT |p2|))
           (OR (NOT |p2|) |p5| (NOT |p1|)) (OR (NOT |p6|) |p5| |p3|)))
(*NT* (AND (OR |p3| |p2| (NOT |p4|)) (OR (NOT |p6|) |p1| (NOT |p4|))
           (OR (NOT |p3|) (NOT |p1|) |p6|) (OR |p3| (NOT |p5|) |p6|)
           (OR |p4| |p2| (NOT |p3|)) (OR (NOT |p2|) (NOT |p3|) |p6|)))
(*NT* (AND (OR |p6| |p2| (NOT |p4|))
           (OR (NOT |p2|) (NOT |p4|) (NOT |p5|))
           (OR (NOT |p4|) (NOT |p6|) |p3|) (OR (NOT |p6|) |p5| |p2|)
           (OR |p1| (NOT |p3|) |p5|) (OR |p3| |p1| (NOT |p5|))))
(*NT* (AND (OR (NOT |p3|) (NOT |p6|) |p1|) (OR (NOT |p6|) |p3| |p4|)
           (OR (NOT |p5|) |p2| |p1|) (OR (NOT |p6|) |p5| (NOT |p2|))
           (OR (NOT |p6|) |p4| (NOT |p3|)) (OR (NOT |p1|) |p4| |p6|)
           (OR |p2| (NOT |p3|) |p4|) (OR (NOT |p2|) |p3| |p4|)))
(*NT* (AND (OR (NOT |p5|) |p3| (NOT |p4|)) (OR |p1| (NOT |p5|) |p2|)
           (OR (NOT |p6|) (NOT |p4|) |p2|)
           (OR (NOT |p3|) (NOT |p1|) (NOT |p4|))
           (OR |p4| (NOT |p2|) (NOT |p3|)) (OR |p5| (NOT |p3|) |p2|)
           (OR (NOT |p6|) |p5| |p2|) (OR |p1| |p2| |p4|)))
(*NT* (AND (OR (NOT |p2|) (NOT |p6|) |p3|)
           (OR (NOT |p5|) (NOT |p3|) |p2|) (OR |p3| |p4| |p6|)
           (OR |p4| (NOT |p3|) |p2|)
           (OR (NOT |p4|) (NOT |p6|) (NOT |p2|))
           (OR |p3| |p6| (NOT |p1|)) (OR |p4| |p3| (NOT |p2|))
           (OR (NOT |p3|) |p1| (NOT |p2|))))
(*NT* (AND (OR |p4| |p6| |p3|) (OR |p3| |p6| (NOT |p5|))
           (OR (NOT |p6|) |p5| |p4|) (OR (NOT |p1|) |p4| |p3|)
           (OR |p2| (NOT |p4|) |p6|) (OR |p2| (NOT |p6|) |p1|)
           (OR |p2| |p5| |p6|) (OR (NOT |p6|) |p4| |p2|)))
(*NT* (AND (OR (NOT |p2|) |p3| |p5|)
           (OR (NOT |p5|) (NOT |p2|) (NOT |p1|))
           (OR (NOT |p2|) (NOT |p4|) |p6|)
           (OR (NOT |p1|) |p4| (NOT |p3|)) (OR |p5| |p4| (NOT |p1|))
           (OR |p2| (NOT |p5|) |p1|) (OR |p4| (NOT |p3|) |p2|)
           (OR (NOT |p6|) (NOT |p3|) (NOT |p1|))))
(*NT* (AND (OR (NOT |p5|) (NOT |p2|) |p6|) (OR |p5| |p1| (NOT |p4|))
           (OR |p5| |p2| |p4|) (OR (NOT |p5|) (NOT |p2|) (NOT |p3|))
           (OR |p5| (NOT |p2|) |p6|) (OR (NOT |p4|) (NOT |p5|) |p3|)
           (OR |p3| |p6| (NOT |p2|)) (OR |p6| (NOT |p5|) (NOT |p3|))))
(*NT* (AND (OR |p3| (NOT |p2|) |p4|)
           (OR (NOT |p4|) (NOT |p5|) (NOT |p6|))
           (OR (NOT |p2|) (NOT |p4|) |p6|)
           (OR (NOT |p5|) |p3| (NOT |p4|)) (OR |p3| |p2| |p5|)
           (OR (NOT |p1|) |p4| (NOT |p2|))
           (OR (NOT |p3|) (NOT |p1|) (NOT |p2|))
           (OR (NOT |p5|) (NOT |p3|) |p6|)))
(*NT* (AND (OR |p6| (NOT |p4|) |p1|) (OR |p2| (NOT |p1|) (NOT |p3|))
           (OR |p5| (NOT |p1|) (NOT |p3|))
           (OR (NOT |p3|) (NOT |p2|) |p4|)
           (OR (NOT |p6|) (NOT |p3|) |p4|) (OR (NOT |p2|) |p3| |p4|)
           (OR (NOT |p6|) |p4| |p5|) (OR |p3| (NOT |p2|) |p4|)))