The mouse sees the tiger. The tiger sees the mouse. If the tiger is round and the tiger is not young then the tiger does not eat the mouse.
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the tiger is round and the tiger is not young then the tiger does not eat the mouse.
((("tiger" "is" "round" "+") ("tiger" "is" "young" "~")) -> ("tiger" "eats" "mouse" "-"))
The tiger sees the mouse.
True
1
proof
[(triple2)]
("tiger" "sees" "mouse" "+")
triple2
The tiger does not see the mouse.
False
1
inv-proof
[(triple2)]
("tiger" "sees" "mouse" "-")
triple2
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The mouse sees the tiger.[(triple1)] The tiger sees the mouse.[(triple2)]
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple2