The dog visits the rabbit. The mouse visits the dog. The rabbit is green. If something likes the rabbit then the rabbit visits the dog. If something visits the rabbit then the rabbit visits the dog. If something likes the rabbit and the rabbit is young then the rabbit likes the dog. If something likes the rabbit and the rabbit sees the mouse then the rabbit is cold. If something visits the rabbit and the rabbit visits the mouse then it is nice. If something sees the dog then it likes the dog. If something is green then it visits the rabbit. If the mouse likes the dog and the dog visits the mouse then the dog is green.
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
If something likes the rabbit then the rabbit visits the dog.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If something visits the rabbit then the rabbit visits the dog.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
If something likes the rabbit and the rabbit is young then the rabbit likes the dog.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "likes" "dog" "+"))
If something likes the rabbit and the rabbit sees the mouse then the rabbit is cold.
((("something" "likes" "rabbit" "+") ("rabbit" "sees" "mouse" "+")) -> ("rabbit" "is" "cold" "+"))
If something visits the rabbit and the rabbit visits the mouse then it is nice.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something sees the dog then it likes the dog.
((("something" "sees" "dog" "+")) -> ("something" "likes" "dog" "+"))
If something is green then it visits the rabbit.
((("something" "is" "green" "+")) -> ("something" "visits" "rabbit" "+"))
If the mouse likes the dog and the dog visits the mouse then the dog is green.
((("mouse" "likes" "dog" "+") ("dog" "visits" "mouse" "+")) -> ("dog" "is" "green" "+"))
The mouse visits the dog.
True
1
proof
[(triple2)]
("mouse" "visits" "dog" "+")
triple2
The mouse does not visit the dog.
False
1
inv-proof
[(triple2)]
("mouse" "visits" "dog" "-")
triple2
The rabbit visits the dog.
True
2
proof
[(((triple1) -> rule2) OR ((((triple3) -> rule7)) -> rule2))]
("rabbit" "visits" "dog" "+")
((triple1) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule2) OR ((((triple3) -> rule7)) -> rule2))]
("rabbit" "visits" "dog" "-")
((triple1) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "dog" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "dog" "+")
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 mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The dog visits the rabbit.[(triple1)] The mouse visits the dog.[(triple2)] The rabbit is green.[(triple3)] @1: The rabbit visits the dog.[(((triple1) -> rule2) OR ((((triple3) -> rule7)) -> rule2))] The rabbit visits the rabbit.[(((triple3) -> rule7))]
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple1) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple3) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1