The cow chases the rabbit. The rabbit visits the tiger. The tiger is nice. If someone is big and they see the tiger then they chase the tiger. If someone sees the cow and they chase the cow then the cow sees the tiger.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone is big and they see the tiger then they chase the tiger.
((("someone" "is" "big" "+") ("someone" "sees" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
If someone sees the cow and they chase the cow then the cow sees the tiger.
((("someone" "sees" "cow" "+") ("someone" "chases" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple3)]
("tiger" "is" "nice" "+")
triple3
The tiger is not nice.
False
1
inv-proof
[(triple3)]
("tiger" "is" "nice" "-")
triple3
The cow does not see the tiger.
Unknown
inv-rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "tiger" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The cow chases the rabbit.[(triple1)] The rabbit visits the tiger.[(triple2)] The tiger is nice.[(triple3)]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple2
The tiger is nice.
("tiger" "is" "nice" "+")
triple3