The dog chases the rabbit. The dog likes the rabbit. The rabbit is big. If the rabbit is big then the rabbit visits the dog. If the rabbit likes the dog and the rabbit is not red then the rabbit does not visit the dog.
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If the rabbit is big then the rabbit visits the dog.
((("rabbit" "is" "big" "+")) -> ("rabbit" "visits" "dog" "+"))
If the rabbit likes the dog and the rabbit is not red then the rabbit does not visit the dog.
((("rabbit" "likes" "dog" "+") ("rabbit" "is" "red" "~")) -> ("rabbit" "visits" "dog" "-"))
The dog chases the rabbit.
True
1
proof
[(triple1)]
("dog" "chases" "rabbit" "+")
triple1
The rabbit is not big.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "big" "-")
triple3
The rabbit visits the dog.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "visits" "dog" "+")
((triple3) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit does not visit the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "visits" "dog" "-")
((triple3) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog does not visit the rabbit.
Unknown
inv-random
[@0: The dog visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "rabbit" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The dog chases the rabbit.[(triple1)] The dog likes the rabbit.[(triple2)] The rabbit is big.[(triple3)] @1: The rabbit visits the dog.[(((triple3) -> rule1))]
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple3) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1