-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathformulas.txt
20 lines (19 loc) · 1.58 KB
/
formulas.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
EXAMPLE, expected = "f(g(x)) = g(f(x)) & f(g(f(y))) = x & f(y) = x & g(f(x)) != x", "UNSAT"
EXAMPLE, expected = "f(g(x)) = g(f(x)) & f(g(f(y))) = x & f(y) = x & g(f(x)) != y", "SAT"
EXAMPLE, expected = "f(a) = b & f(f(a)) = c & g(c, f(b)) != g(c, c)", "UNSAT"
EXAMPLE, expected = "f(f(f(a))) = f(f(a)) & f(f(f(f(a)))) = a & f(a) != a", "UNSAT"
EXAMPLE, expected = "f(f(f(a))) = a & f(f(f(f(f(a))))) = a & f(a) != a","UNSAT"
EXAMPLE, expected = "f(f(f(a))) = f(a) & f(f(a)) = a & f(a) != a", "SAT"
EXAMPLE, expected = "f(f(f(a))) = f(a) & f(f(a)) = a & f(f(f(f(a)))) != a", "UNSAT"
EXAMPLE, expected = "f(a) =b & f(b)= f(g(a)) &f(a)!=b", "UNSAT"
EXAMPLE, expected = "f(a, b) =b & f(b,c)= f(g(a), b) &f(a,c)!=b", "SAT"
EXAMPLE, expected = "f(a,b) = a & f(f(a,b), b) != a", "UNSAT"
EXAMPLE, expected = "a = b & b = c & f(a) = f(c) & g(f(a)) = g(f(b)) & g(f(a)) != h(d)", "SAT"
EXAMPLE, expected = "p(x) = q(y) & q(y) = r(z) & p(x) = r(z) & s(p(x)) != t(q(y))", "SAT"
EXAMPLE, expected = "f(a) = g(b) & g(b) = h(c) & h(c) = f(d) & a = d & f(a) != k(e)", "SAT"
EXAMPLE, expected = "a = b & b = c & f(a) = f(b) & f(c) = g(d) & g(d) = f(a) & f(a) != g(d)", "UNSAT"
EXAMPLE, expected = "p(x) = q(y) & q(y) = r(z) & p(x) = r(z) & s(p(x)) = t(q(y)) & t(q(y)) != s(r(z))", "UNSAT"
EXAMPLE, expected = "f(a) = g(b) & g(b) = h(c) & h(c) = f(a) & f(a) = k(d) & k(d) != f(a)", "UNSAT"
EXAMPLE, expected = "f(a,b) = a & f(f(a,b), b) != a", "UNSAT"
EXAMPLE, expected = "f(g(x)) = g(f(x)) & f(g(f(y))) = x & f(y) = x & g(f(x)) != y", "SAT"
EXAMPLE, expected = "f(g(x)) = g(f(x)) & f(g(f(y))) = x & f(y) = x & g(f(x)) != x", "UNSAT"