The dog sees the rabbit. The rabbit sees the dog. If someone is blue then they visit the rabbit. If someone sees the dog then the dog visits the rabbit. If someone likes the dog and they do not visit the dog then they like the rabbit.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone is blue then they visit the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone sees the dog then the dog visits the rabbit.
((("someone" "sees" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If someone likes the dog and they do not visit the dog then they like the rabbit.
((("someone" "likes" "dog" "+") ("someone" "visits" "dog" "~")) -> ("someone" "likes" "rabbit" "+"))
The dog sees the rabbit.
True
1
proof
[(triple1)]
("dog" "sees" "rabbit" "+")
triple1
The rabbit does not see the dog.
False
1
inv-proof
[(triple2)]
("rabbit" "sees" "dog" "-")
triple2
The dog visits the rabbit.
True
2
proof
[(((triple2) -> rule2))]
("dog" "visits" "rabbit" "+")
((triple2) -> (rule2 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The dog does not visit the rabbit.
False
2
inv-proof
[(((triple2) -> rule2))]
("dog" "visits" "rabbit" "-")
((triple2) -> (rule2 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The dog likes the rabbit.
Unknown
rconc
[@1: The dog likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "rabbit" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The dog sees the rabbit.[(triple1)] The rabbit sees the dog.[(triple2)] @1: The dog visits the rabbit.[(((triple2) -> rule2))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple2
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple2) -> (rule2 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1