aboutsummaryrefslogtreecommitdiff
path: root/data
diff options
context:
space:
mode:
Diffstat (limited to 'data')
-rw-r--r--data/simple_propositional.p5
1 files changed, 5 insertions, 0 deletions
diff --git a/data/simple_propositional.p b/data/simple_propositional.p
new file mode 100644
index 0000000..283c326
--- /dev/null
+++ b/data/simple_propositional.p
@@ -0,0 +1,5 @@
+% Simple propositional-style test
+% P(a) and (P(X) → Q(X)) and ¬Q(a) should be unsatisfiable.
+cnf(fact, axiom, p(a)).
+cnf(rule, axiom, ~p(X) | q(X)).
+cnf(goal, negated_conjecture, ~q(a)).