The cow is nice. The cow visits the dog. The dog sees the cow. If something is young and it likes the cow then the cow sees the dog. If something is blue and it does not like the cow then the cow sees the dog. If something sees the cow then it is not blue.
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If something is young and it likes the cow then the cow sees the dog.
((("something" "is" "young" "+") ("something" "likes" "cow" "+")) -> ("cow" "sees" "dog" "+"))
If something is blue and it does not like the cow then the cow sees the dog.
((("something" "is" "blue" "+") ("something" "likes" "cow" "~")) -> ("cow" "sees" "dog" "+"))
If something sees the cow then it is not blue.
((("something" "sees" "cow" "+")) -> ("something" "is" "blue" "-"))
The cow visits the dog.
True
1
proof
[(triple2)]
("cow" "visits" "dog" "+")
triple2
The cow is not nice.
False
1
inv-proof
[(triple1)]
("cow" "is" "nice" "-")
triple1
The cow does not see the dog.
Unknown
inv-rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cow is nice.[(triple1)] The cow visits the dog.[(triple2)] The dog sees the cow.[(triple3)] @1: The dog is not blue.[(((triple3) -> rule3))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow visits the dog.
("cow" "visits" "dog" "+")
triple2
The dog sees the cow.
("dog" "sees" "cow" "+")
triple3
The dog is not blue.
("dog" "is" "blue" "-")
((triple3) -> (rule3 % int1))
The dog is not blue.
("dog" "is" "blue" "-")
int1