The cat sees the mouse. The lion likes the cat. The mouse is red. If something is green and it sees the cat then the cat likes the mouse. If something is nice then it needs the lion. If something is young and it likes the mouse then it is nice. If something likes the mouse then it sees the mouse. Red things are nice. If something sees the cat then it likes the cat.
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The mouse is red.
("mouse" "is" "red" "+")
If something is green and it sees the cat then the cat likes the mouse.
((("something" "is" "green" "+") ("something" "sees" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If something is nice then it needs the lion.
((("something" "is" "nice" "+")) -> ("something" "needs" "lion" "+"))
If something is young and it likes the mouse then it is nice.
((("something" "is" "young" "+") ("something" "likes" "mouse" "+")) -> ("something" "is" "nice" "+"))
If something likes the mouse then it sees the mouse.
((("something" "likes" "mouse" "+")) -> ("something" "sees" "mouse" "+"))
Red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something sees the cat then it likes the cat.
((("something" "sees" "cat" "+")) -> ("something" "likes" "cat" "+"))
The cat sees the mouse.
True
1
proof
[(triple1)]
("cat" "sees" "mouse" "+")
triple1
The lion does not like the cat.
False
1
inv-proof
[(triple2)]
("lion" "likes" "cat" "-")
triple2
The cat does not like the mouse.
Unknown
inv-rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "mouse" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
@0: The cat sees the mouse.[(triple1)] The lion likes the cat.[(triple2)] The mouse is red.[(triple3)] @1: The mouse is nice.[(((triple3) -> rule5))] @2: The mouse needs the lion.[(((((triple3) -> rule5)) -> rule2))]
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple1
The lion likes the cat.
("lion" "likes" "cat" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
((triple3) -> (rule5 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2