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