The bear is cold. The dog visits the rabbit. The mouse needs the rabbit. The rabbit visits the mouse. If something visits the dog then it visits the mouse.
The bear is cold.
("bear" "is" "cold" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something visits the dog then it visits the mouse.
((("something" "visits" "dog" "+")) -> ("something" "visits" "mouse" "+"))
The dog visits the rabbit.
True
1
proof
[(triple2)]
("dog" "visits" "rabbit" "+")
triple2
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple4)]
("rabbit" "visits" "mouse" "-")
triple4
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The rabbit chases the mouse.
Unknown
random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "+")
@0: The bear is cold.[(triple1)] The dog visits the rabbit.[(triple2)] The mouse needs the rabbit.[(triple3)] The rabbit visits the mouse.[(triple4)]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple3
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple4