The cat is red. The mouse is round. The tiger likes the cat. If something visits the mouse and the mouse likes the tiger then the mouse visits the tiger. If the cat eats the tiger then the tiger visits the cat.
The cat is red.
("cat" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something visits the mouse and the mouse likes the tiger then the mouse visits the tiger.
((("something" "visits" "mouse" "+") ("mouse" "likes" "tiger" "+")) -> ("mouse" "visits" "tiger" "+"))
If the cat eats the tiger then the tiger visits the cat.
((("cat" "eats" "tiger" "+")) -> ("tiger" "visits" "cat" "+"))
The mouse is round.
True
1
proof
[(triple2)]
("mouse" "is" "round" "+")
triple2
The mouse is not round.
False
1
inv-proof
[(triple2)]
("mouse" "is" "round" "-")
triple2
The mouse does not visit the tiger.
Unknown
inv-rconc
[@1: The mouse visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "tiger" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The cat is red.[(triple1)] The mouse is round.[(triple2)] The tiger likes the cat.[(triple3)]
The cat is red.
("cat" "is" "red" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple3