The dog likes the mouse. The mouse eats the squirrel. The rabbit is red. The squirrel visits the dog. If someone is red and they do not visit the rabbit then the rabbit does not visit the dog. If the mouse eats the squirrel then the mouse likes the rabbit. If someone likes the rabbit and they are not green then they like the dog.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone is red and they do not visit the rabbit then the rabbit does not visit the dog.
((("someone" "is" "red" "+") ("someone" "visits" "rabbit" "~")) -> ("rabbit" "visits" "dog" "-"))
If the mouse eats the squirrel then the mouse likes the rabbit.
((("mouse" "eats" "squirrel" "+")) -> ("mouse" "likes" "rabbit" "+"))
If someone likes the rabbit and they are not green then they like the dog.
((("someone" "likes" "rabbit" "+") ("someone" "is" "green" "~")) -> ("someone" "likes" "dog" "+"))
The squirrel visits the dog.
True
1
proof
[(triple4)]
("squirrel" "visits" "dog" "+")
triple4
The dog does not like the mouse.
False
1
inv-proof
[(triple1)]
("dog" "likes" "mouse" "-")
triple1
The mouse likes the rabbit.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "likes" "rabbit" "+")
((triple2) -> (rule2 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse does not like the rabbit.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "likes" "rabbit" "-")
((triple2) -> (rule2 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "dog" "-")
The mouse likes the dog.
Unknown
rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "dog" "+")
The mouse does not eat the rabbit.
Unknown
inv-random
[@0: The mouse eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "rabbit" "-")
The dog likes the squirrel.
Unknown
random
[@0: The dog likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "squirrel" "+")
@0: The dog likes the mouse.[(triple1)] The mouse eats the squirrel.[(triple2)] The rabbit is red.[(triple3)] The squirrel visits the dog.[(triple4)] @1: The mouse likes the rabbit.[(((triple2) -> rule2))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((triple2) -> (rule2 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1