The cat needs the cow. The cat needs the lion. The cow likes the cat. The lion is red. The lion needs the rabbit. The lion sees the cow. The rabbit is green. The rabbit is kind. The rabbit likes the lion. The rabbit sees the lion. If someone likes the cat and the cat needs the cow then they are nice. If the lion sees the rabbit then the rabbit is green. If the cow needs the rabbit then the rabbit is nice.
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone likes the cat and the cat needs the cow then they are nice.
((("someone" "likes" "cat" "+") ("cat" "needs" "cow" "+")) -> ("someone" "is" "nice" "+"))
If the lion sees the rabbit then the rabbit is green.
((("lion" "sees" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If the cow needs the rabbit then the rabbit is nice.
((("cow" "needs" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
The rabbit is green.
True
1
proof
[(triple7)]
("rabbit" "is" "green" "+")
triple7
The rabbit does not see the lion.
False
1
inv-proof
[(triple10)]
("rabbit" "sees" "lion" "-")
triple10
The cow is nice.
True
3
proof
[(((triple3 triple1) -> rule1))]
("cow" "is" "nice" "+")
((triple3 triple1) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
3
inv-proof
[(((triple3 triple1) -> rule1))]
("cow" "is" "nice" "-")
((triple3 triple1) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "nice" "-")
The cat is nice.
Unknown
rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The cat needs the cow.[(triple1)] The cat needs the lion.[(triple2)] The cow likes the cat.[(triple3)] The lion is red.[(triple4)] The lion needs the rabbit.[(triple5)] The lion sees the cow.[(triple6)] The rabbit is green.[(triple7)] The rabbit is kind.[(triple8)] The rabbit likes the lion.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The cow is nice.[(((triple3 triple1) -> rule1))]
The cat needs the cow.
("cat" "needs" "cow" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple5
The lion sees the cow.
("lion" "sees" "cow" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The cow is nice.
("cow" "is" "nice" "+")
((triple3 triple1) -> (rule1 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1