The lion chases the rabbit. The lion is rough. The rabbit is rough. If someone is rough and they like the rabbit then they like the lion. If someone is big then they see the rabbit. If someone likes the rabbit then they are rough.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is rough.
("lion" "is" "rough" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If someone is rough and they like the rabbit then they like the lion.
((("someone" "is" "rough" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "likes" "lion" "+"))
If someone is big then they see the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone likes the rabbit then they are rough.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
The lion is rough.
True
1
proof
[(triple2)]
("lion" "is" "rough" "+")
triple2
The rabbit is not rough.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "rough" "-")
triple3
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "lion" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is rough.[(triple2)] The rabbit is rough.[(triple3)]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple3