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