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