The bear visits the mouse. The cat visits the bear. The mouse eats the cat. If the mouse visits the cat and the mouse likes the cat then the cat is nice. If something visits the bear then the bear visits the cat.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
If the mouse visits the cat and the mouse likes the cat then the cat is nice.
((("mouse" "visits" "cat" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something visits the bear then the bear visits the cat.
((("something" "visits" "bear" "+")) -> ("bear" "visits" "cat" "+"))
The bear visits the mouse.
True
1
proof
[(triple1)]
("bear" "visits" "mouse" "+")
triple1
The mouse does not eat the cat.
False
1
inv-proof
[(triple3)]
("mouse" "eats" "cat" "-")
triple3
The bear visits the cat.
True
2
proof
[(((triple2) -> rule2))]
("bear" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "visits" "cat" "-")
((triple2) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
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 visits the bear.
Unknown
random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "+")
@0: The bear visits the mouse.[(triple1)] The cat visits the bear.[(triple2)] The mouse eats the cat.[(triple3)] @1: The bear visits the cat.[(((triple2) -> rule2))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple3
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1