The mouse is nice. The mouse likes the rabbit. The rabbit is young. If something is nice and it likes the rabbit then the rabbit likes the mouse. If something is round then it likes the mouse. If the rabbit visits the mouse and the mouse sees the rabbit then the mouse likes the rabbit.
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If something is nice and it likes the rabbit then the rabbit likes the mouse.
((("something" "is" "nice" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something is round then it likes the mouse.
((("something" "is" "round" "+")) -> ("something" "likes" "mouse" "+"))
If the rabbit visits the mouse and the mouse sees the rabbit then the mouse likes the rabbit.
((("rabbit" "visits" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("mouse" "likes" "rabbit" "+"))
The mouse is nice.
True
1
proof
[(triple1)]
("mouse" "is" "nice" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "young" "-")
triple3
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse visits the rabbit.
Unknown
random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "+")
@0: The mouse is nice.[(triple1)] The mouse likes the rabbit.[(triple2)] The rabbit is young.[(triple3)] @1: The rabbit likes the mouse.[(((triple1 triple2) -> rule1))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple2
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((triple1 triple2) -> (rule1 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1