(note TQG40)  ;; boolean version

;; Predicate introduction.

(instance testPred40-1 BinaryPredicate)
(domain testPred40-1 1 Entity)
(domain testPred40-1 2 Entity)
(instance Entity40-1 Entity)
(instance Entity40-2 Entity)
(instance Entity40-3 Entity)

(query (not (testPred40-1 Entity40-1 Entity40-2 Entity40-3)))

(answer yes)


;; This test fails because there are no axioms to prevent a
;; BinaryPredicate from being used to form a statement with three
;; arguments.  (Such axioms cause problems of their own.)  This sort
;; of syntactic correctness enforcement probably should not be done in
;; inference, but as part of a canonicalization/rejection step that
;; prevents non-wff expressions from ever reaching the inference
;; engine.