Tauts:

t1. (testTaut '(O a (N a)))

t2. (testTaut '(O (A a b (N a) (N b)) (N (A a b (N a) (N b)))))

t3. (testTaut '(O p (O (N p) q) (O (N q) r) (O (N r) s) (N s) s))

t4. (testTaut '(O (N (O (N p) q)) (O q (N p))))

t5. (testTaut '(O (N a) (O (N b) a)))

t6. (testTaut '(O (N (A a b)) a))

t7. (testTaut '(O (N a) (O a b)))

t8. (testTaut '(O (N (O (N a) b)) (O (N (O (N a) (O (N b) c))) (O (N a) c))))


Satisfiable:

s1. (testTaut '(O a b))

s2. (testTaut '(A a b c (N a) (N b) (N c)))

s3. (testTaut '(N (O (A a b (N a) (N b)) (N (A a b (N a) (N b))))))

s4. (testTaut '(A (O p q) (O (N q) r) (O (N p) r) (N r)))

s5. (testTaut '(A p (O (N p) q) (O (N q) r) (O (N r) s) (N s) s))

s6. (testTaut '(O (N (A (O p q) (O r s))) (A (O r q) (O r s))))