The cat does not chase the lion. The cat is kind. The cat is rough. The cat needs the cow. The cow chases the cat. The cow chases the rabbit. The cow is cold. The cow is kind. The cow does not need the rabbit. The cow visits the lion. The lion chases the cow. The lion chases the rabbit. The lion does not visit the rabbit. The rabbit does not chase the cat. The rabbit chases the lion. The rabbit is rough. If someone chases the cat and the cat chases the cow then the cow chases the cat. If someone chases the cat then they chase the cow. If someone chases the cow and they are cold then the cow is cold. If someone chases the cow and the cow does not chase the cat then the cow visits the cat. If someone visits the cat then they need the cat. If the cow visits the rabbit and the cow visits the cat then the rabbit visits the lion.
The cat does not chase the lion.
("cat" "chases" "lion" "-")
The cat is kind.
("cat" "is" "kind" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If someone chases the cat and the cat chases the cow then the cow chases the cat.
((("someone" "chases" "cat" "+") ("cat" "chases" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If someone chases the cat then they chase the cow.
((("someone" "chases" "cat" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow and they are cold then the cow is cold.
((("someone" "chases" "cow" "+") ("someone" "is" "cold" "+")) -> ("cow" "is" "cold" "+"))
If someone chases the cow and the cow does not chase the cat then the cow visits the cat.
((("someone" "chases" "cow" "+") ("cow" "chases" "cat" "~")) -> ("cow" "visits" "cat" "+"))
If someone visits the cat then they need the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "cat" "+"))
If the cow visits the rabbit and the cow visits the cat then the rabbit visits the lion.
((("cow" "visits" "rabbit" "+") ("cow" "visits" "cat" "+")) -> ("rabbit" "visits" "lion" "+"))
The cat is rough.
True
1
proof
[(triple3)]
("cat" "is" "rough" "+")
triple3
The rabbit chases the cat.
False
1
inv-proof
[(triple14)]
("rabbit" "chases" "cat" "+")
triple14
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "cow" "-")
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 does not chase the lion.[(triple1)] The cat is kind.[(triple2)] The cat is rough.[(triple3)] The cat needs the cow.[(triple4)] The cow chases the cat.[(triple5)] The cow chases the rabbit.[(triple6)] The cow does not need the rabbit.[(triple9)] The cow is cold.[(triple7)] The cow is kind.[(triple8)] The cow visits the lion.[(triple10)] The lion chases the cow.[(triple11)] The lion chases the rabbit.[(triple12)] The lion does not visit the rabbit.[(triple13)] The rabbit chases the lion.[(triple15)] The rabbit does not chase the cat.[(triple14)] The rabbit is rough.[(triple16)] @1: The cow chases the cow.[(((triple5) -> rule2))]
The cat does not chase the lion.
("cat" "chases" "lion" "-")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat needs the cow.
("cat" "needs" "cow" "+")
triple4
The cow chases the cat.
("cow" "chases" "cat" "+")
triple5
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple6
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
triple9
The cow is cold.
("cow" "is" "cold" "+")
triple7
The cow is kind.
("cow" "is" "kind" "+")
triple8
The cow visits the lion.
("cow" "visits" "lion" "+")
triple10
The lion chases the cow.
("lion" "chases" "cow" "+")
triple11
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple12
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
triple13
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple15
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple14
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple16
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple5) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1