The lion is nice. The rabbit eats the lion. The rabbit sees the lion. If someone sees the rabbit then the rabbit sees the lion.
The lion is nice.
("lion" "is" "nice" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone sees the rabbit then the rabbit sees the lion.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "lion" "+"))
The lion is nice.
True
1
proof
[(triple1)]
("lion" "is" "nice" "+")
triple1
The rabbit does not see the lion.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "lion" "-")
triple3
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The lion is nice.[(triple1)] The rabbit eats the lion.[(triple2)] The rabbit sees the lion.[(triple3)]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple2
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple3