The cat eats the rabbit. The cat is blue. The mouse eats the cat. The mouse sees the rabbit. The rabbit sees the mouse. The rabbit visits the mouse. The squirrel visits the rabbit. If something visits the cat and it eats the rabbit then the rabbit sees the cat. If something visits the mouse then the mouse visits the squirrel.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If something visits the cat and it eats the rabbit then the rabbit sees the cat.
((("something" "visits" "cat" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If something visits the mouse then the mouse visits the squirrel.
((("something" "visits" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
The mouse eats the cat.
True
1
proof
[(triple3)]
("mouse" "eats" "cat" "+")
triple3
The squirrel does not visit the rabbit.
False
1
inv-proof
[(triple7)]
("squirrel" "visits" "rabbit" "-")
triple7
The mouse visits the squirrel.
True
2
proof
[(((triple6) -> rule2))]
("mouse" "visits" "squirrel" "+")
((triple6) -> (rule2 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse does not visit the squirrel.
False
2
inv-proof
[(((triple6) -> rule2))]
("mouse" "visits" "squirrel" "-")
((triple6) -> (rule2 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat eats the rabbit.[(triple1)] The cat is blue.[(triple2)] The mouse eats the cat.[(triple3)] The mouse sees the rabbit.[(triple4)] The rabbit sees the mouse.[(triple5)] The rabbit visits the mouse.[(triple6)] The squirrel visits the rabbit.[(triple7)] @1: The mouse visits the squirrel.[(((triple6) -> rule2))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat is blue.
("cat" "is" "blue" "+")
triple2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple3
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple4
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple5
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple6
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple7
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple6) -> (rule2 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1