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