The cat is red. The mouse chases the cat. The mouse likes the cat. If someone likes the cat then they need the mouse. If someone needs the cat and the cat is rough then they are red.
The cat is red.
("cat" "is" "red" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If someone likes the cat then they need the mouse.
((("someone" "likes" "cat" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the cat and the cat is rough then they are red.
((("someone" "needs" "cat" "+") ("cat" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
The mouse chases the cat.
True
1
proof
[(triple2)]
("mouse" "chases" "cat" "+")
triple2
The cat is not red.
False
1
inv-proof
[(triple1)]
("cat" "is" "red" "-")
triple1
The mouse needs the mouse.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("mouse" "needs" "mouse" "-")
((triple3) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "-")
The cat needs the mouse.
Unknown
rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "mouse" "+")
The cat does not chase the mouse.
Unknown
inv-random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The cat is red.[(triple1)] The mouse chases the cat.[(triple2)] The mouse likes the cat.[(triple3)] @1: The mouse needs the mouse.[(((triple3) -> rule1))]
The cat is red.
("cat" "is" "red" "+")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple3
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple3) -> (rule1 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1