The mouse is cold. The mouse visits the tiger. The tiger chases the mouse. If someone chases the tiger then they are cold. If someone is round then they like the tiger. If someone likes the mouse and they are cold then they chase the tiger.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
If someone chases the tiger then they are cold.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they like the tiger.
((("someone" "is" "round" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the mouse and they are cold then they chase the tiger.
((("someone" "likes" "mouse" "+") ("someone" "is" "cold" "+")) -> ("someone" "chases" "tiger" "+"))
The mouse visits the tiger.
True
1
proof
[(triple2)]
("mouse" "visits" "tiger" "+")
triple2
The mouse is not cold.
False
1
inv-proof
[(triple1)]
("mouse" "is" "cold" "-")
triple1
The mouse does not chase the tiger.
Unknown
inv-rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "tiger" "-")
The tiger visits the mouse.
Unknown
random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "+")
@0: The mouse is cold.[(triple1)] The mouse visits the tiger.[(triple2)] The tiger chases the mouse.[(triple3)]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple3