The cat visits the mouse. The mouse visits the cat. If something needs the cat then it likes the cat. If something visits the mouse and the mouse visits the cat then it is young. If something likes the mouse and it needs the cat then the cat is cold. If something is young and it likes the cat then the cat is kind. If something needs the cat then it likes the mouse. If the mouse visits the cat then the mouse likes the cat. If something is cold and it needs the mouse then the mouse is kind. If the mouse visits the cat and the cat is young then the mouse likes the cat.
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something needs the cat then it likes the cat.
((("something" "needs" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something visits the mouse and the mouse visits the cat then it is young.
((("something" "visits" "mouse" "+") ("mouse" "visits" "cat" "+")) -> ("something" "is" "young" "+"))
If something likes the mouse and it needs the cat then the cat is cold.
((("something" "likes" "mouse" "+") ("something" "needs" "cat" "+")) -> ("cat" "is" "cold" "+"))
If something is young and it likes the cat then the cat is kind.
((("something" "is" "young" "+") ("something" "likes" "cat" "+")) -> ("cat" "is" "kind" "+"))
If something needs the cat then it likes the mouse.
((("something" "needs" "cat" "+")) -> ("something" "likes" "mouse" "+"))
If the mouse visits the cat then the mouse likes the cat.
((("mouse" "visits" "cat" "+")) -> ("mouse" "likes" "cat" "+"))
If something is cold and it needs the mouse then the mouse is kind.
((("something" "is" "cold" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse visits the cat and the cat is young then the mouse likes the cat.
((("mouse" "visits" "cat" "+") ("cat" "is" "young" "+")) -> ("mouse" "likes" "cat" "+"))
The mouse visits the cat.
True
1
proof
[(triple2)]
("mouse" "visits" "cat" "+")
triple2
The cat does not visit the mouse.
False
1
inv-proof
[(triple1)]
("cat" "visits" "mouse" "-")
triple1
The cat is young.
True
3
proof
[(((triple1 triple2) -> rule2))]
("cat" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("cat" "is" "young" "-")
((triple1 triple2) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cat" "-")
The cat likes the mouse.
Unknown
rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "mouse" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cat visits the mouse.[(triple1)] The mouse visits the cat.[(triple2)] @1: The cat is young.[(((triple1 triple2) -> rule2))] The mouse likes the cat.[(((triple2) -> rule6) OR ((triple2 ((triple1 triple2) -> rule2)) -> rule8))]
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple2) -> (rule6 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
((triple2 ((triple1 triple2) -> (rule2 % int2))) -> (rule8 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2