The cat is red. The cat likes the cow. The cat visits the cow. The cat visits the rabbit. The cow is red. The cow likes the cat. The cow does not like the rabbit. The cow needs the rabbit. The cow visits the cat. The cow does not visit the rabbit. The rabbit is big. The rabbit is green. The rabbit is kind. The rabbit is red. The rabbit needs the cat. If someone is kind and they like the cat then they need the cat. If someone likes the rabbit then they are red. If someone likes the cat then they visit the cow.
The cat is red.
("cat" "is" "red" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow does not like the rabbit.
("cow" "likes" "rabbit" "-")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
If someone is kind and they like the cat then they need the cat.
((("someone" "is" "kind" "+") ("someone" "likes" "cat" "+")) -> ("someone" "needs" "cat" "+"))
If someone likes the rabbit then they are red.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone likes the cat then they visit the cow.
((("someone" "likes" "cat" "+")) -> ("someone" "visits" "cow" "+"))
The cow does not visit the rabbit.
True
1
proof
[(triple10)]
("cow" "visits" "rabbit" "-")
triple10
The cow visits the rabbit.
False
1
inv-proof
[(triple10)]
("cow" "visits" "rabbit" "+")
triple10
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The rabbit needs the cow.
Unknown
random
[@0: The rabbit needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cow" "+")
@0: The cat is red.[(triple1)] The cat likes the cow.[(triple2)] The cat visits the cow.[(triple3)] The cat visits the rabbit.[(triple4)] The cow does not like the rabbit.[(triple7)] The cow does not visit the rabbit.[(triple10)] The cow is red.[(triple5)] The cow likes the cat.[(triple6)] The cow needs the rabbit.[(triple8)] The cow visits the cat.[(triple9)] The rabbit is big.[(triple11)] The rabbit is green.[(triple12)] The rabbit is kind.[(triple13)] The rabbit is red.[(triple14)] The rabbit needs the cat.[(triple15)] @1: The cow visits the cow.[(((triple6) -> rule3))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple4
The cow does not like the rabbit.
("cow" "likes" "rabbit" "-")
triple7
The cow does not visit the rabbit.
("cow" "visits" "rabbit" "-")
triple10
The cow is red.
("cow" "is" "red" "+")
triple5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple6
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple8
The cow visits the cat.
("cow" "visits" "cat" "+")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit is red.
("rabbit" "is" "red" "+")
triple14
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple15
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple6) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1