The bear visits the tiger. The cat needs the bear. The rabbit likes the tiger. The tiger visits the rabbit. If someone needs the tiger and the tiger visits the bear then the tiger visits the rabbit. If someone visits the rabbit then the rabbit is not red.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone needs the tiger and the tiger visits the bear then the tiger visits the rabbit.
((("someone" "needs" "tiger" "+") ("tiger" "visits" "bear" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone visits the rabbit then the rabbit is not red.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "red" "-"))
The cat needs the bear.
True
1
proof
[(triple2)]
("cat" "needs" "bear" "+")
triple2
The rabbit does not like the tiger.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "tiger" "-")
triple3
The rabbit is not red.
True
2
proof
[(((triple4) -> rule2))]
("rabbit" "is" "red" "-")
((triple4) -> (rule2 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1
The rabbit is red.
False
2
inv-proof
[(((triple4) -> rule2))]
("rabbit" "is" "red" "+")
((triple4) -> (rule2 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The rabbit does not like the bear.
Unknown
inv-random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear visits the tiger.[(triple1)] The cat needs the bear.[(triple2)] The rabbit likes the tiger.[(triple3)] The tiger visits the rabbit.[(triple4)] @1: The rabbit is not red.[(((triple4) -> rule2))]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The cat needs the bear.
("cat" "needs" "bear" "+")
triple2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple3
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple4
The rabbit is not red.
("rabbit" "is" "red" "-")
((triple4) -> (rule2 % int1))
The rabbit is not red.
("rabbit" "is" "red" "-")
int1