The cat chases the dog. The cat chases the rabbit. The cat eats the dog. The cat does not eat the rabbit. The cat is nice. The cat is red. The cat visits the rabbit. The dog is nice. The dog visits the cat. The rabbit chases the cat. The rabbit eats the cat. The rabbit eats the dog. The rabbit is big. The rabbit is blue. The rabbit visits the cat. The rabbit visits the dog. If something eats the rabbit and it is big then the rabbit does not visit the cat. If something visits the cat then it is nice. If the rabbit visits the dog and the dog eats the rabbit then the dog visits the rabbit.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat does not eat the rabbit.
("cat" "eats" "rabbit" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something eats the rabbit and it is big then the rabbit does not visit the cat.
((("something" "eats" "rabbit" "+") ("something" "is" "big" "+")) -> ("rabbit" "visits" "cat" "-"))
If something visits the cat then it is nice.
((("something" "visits" "cat" "+")) -> ("something" "is" "nice" "+"))
If the rabbit visits the dog and the dog eats the rabbit then the dog visits the rabbit.
((("rabbit" "visits" "dog" "+") ("dog" "eats" "rabbit" "+")) -> ("dog" "visits" "rabbit" "+"))
The cat eats the dog.
True
1
proof
[(triple3)]
("cat" "eats" "dog" "+")
triple3
The cat does not chase the dog.
False
1
inv-proof
[(triple1)]
("cat" "chases" "dog" "-")
triple1
The dog does not visit the rabbit.
Unknown
inv-rconc
[@1: The dog visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "rabbit" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat chases the dog.[(triple1)] The cat chases the rabbit.[(triple2)] The cat does not eat the rabbit.[(triple4)] The cat eats the dog.[(triple3)] The cat is nice.[(triple5)] The cat is red.[(triple6)] The cat visits the rabbit.[(triple7)] The dog is nice.[(triple8 OR ((triple9) -> rule2))] The dog visits the cat.[(triple9)] The rabbit chases the cat.[(triple10)] The rabbit eats the cat.[(triple11)] The rabbit eats the dog.[(triple12)] The rabbit is big.[(triple13)] The rabbit is blue.[(triple14)] The rabbit visits the cat.[(triple15)] The rabbit visits the dog.[(triple16)] @1: The rabbit is nice.[(((triple15) -> rule2))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat does not eat the rabbit.
("cat" "eats" "rabbit" "-")
triple4
The cat eats the dog.
("cat" "eats" "dog" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple7
The dog is nice.
("dog" "is" "nice" "+")
triple8
((triple9) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
triple9
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple10
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple11
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple12
The rabbit is big.
("rabbit" "is" "big" "+")
triple13
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple14
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple16
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple15) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1