The cat does not like the mouse. The cat visits the mouse. The mouse visits the cat. If someone is nice then they eat the mouse. If someone visits the cat then the cat is not red.
The cat does not like the mouse.
("cat" "likes" "mouse" "-")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone is nice then they eat the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "mouse" "+"))
If someone visits the cat then the cat is not red.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "red" "-"))
The cat visits the mouse.
True
1
proof
[(triple2)]
("cat" "visits" "mouse" "+")
triple2
The cat likes the mouse.
False
1
inv-proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The cat is not red.
True
2
proof
[(((triple3) -> rule2))]
("cat" "is" "red" "-")
((triple3) -> (rule2 % int1))
The cat is not red.
("cat" "is" "red" "-")
int1
The cat is red.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "is" "red" "+")
((triple3) -> (rule2 % int1))
The cat is not red.
("cat" "is" "red" "-")
int1
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The cat eats the mouse.
Unknown
rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "mouse" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cat does not like the mouse.[(triple1)] The cat visits the mouse.[(triple2)] The mouse visits the cat.[(triple3)] @1: The cat is not red.[(((triple3) -> rule2))]
The cat does not like the mouse.
("cat" "likes" "mouse" "-")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple3
The cat is not red.
("cat" "is" "red" "-")
((triple3) -> (rule2 % int1))
The cat is not red.
("cat" "is" "red" "-")
int1