The cat eats the mouse. The mouse does not like the cat. If someone chases the cat then they like the mouse. If someone is green then they do not like the mouse. If someone chases the mouse then they do not eat the cat. If someone is blue then they do not eat the mouse. If the mouse is blue and the mouse is kind then the mouse is nice. If someone eats the mouse then the mouse eats the cat. If someone is green and they eat the mouse then the mouse does not like the cat. If someone likes the cat and they chase the mouse then the cat is nice.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
If someone chases the cat then they like the mouse.
((("someone" "chases" "cat" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is green then they do not like the mouse.
((("someone" "is" "green" "+")) -> ("someone" "likes" "mouse" "-"))
If someone chases the mouse then they do not eat the cat.
((("someone" "chases" "mouse" "+")) -> ("someone" "eats" "cat" "-"))
If someone is blue then they do not eat the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "mouse" "-"))
If the mouse is blue and the mouse is kind then the mouse is nice.
((("mouse" "is" "blue" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "is" "nice" "+"))
If someone eats the mouse then the mouse eats the cat.
((("someone" "eats" "mouse" "+")) -> ("mouse" "eats" "cat" "+"))
If someone is green and they eat the mouse then the mouse does not like the cat.
((("someone" "is" "green" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "likes" "cat" "-"))
If someone likes the cat and they chase the mouse then the cat is nice.
((("someone" "likes" "cat" "+") ("someone" "chases" "mouse" "+")) -> ("cat" "is" "nice" "+"))
The cat eats the mouse.
True
1
proof
[(triple1)]
("cat" "eats" "mouse" "+")
triple1
The cat does not eat the mouse.
False
1
inv-proof
[(triple1)]
("cat" "eats" "mouse" "-")
triple1
The mouse eats the cat.
True
2
proof
[(((triple1) -> rule6))]
("mouse" "eats" "cat" "+")
((triple1) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse does not eat the cat.
False
2
inv-proof
[(((triple1) -> rule6))]
("mouse" "eats" "cat" "-")
((triple1) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The cat likes the mouse.
Unknown
rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "mouse" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cat eats the mouse.[(triple1)] The mouse does not like the cat.[(triple2)] @1: The mouse eats the cat.[(((triple1) -> rule6))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((triple1) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1