The lion is not big. The lion is nice. The lion is rough. The lion is young. The lion likes the rabbit. The lion sees the rabbit. The lion visits the rabbit. The rabbit is not big. The rabbit is blue. The rabbit is nice. The rabbit is rough. The rabbit is young. The rabbit likes the lion. The rabbit sees the lion. The rabbit visits the lion. If someone is big and they do not see the lion then the lion visits the rabbit. If the lion is nice and the lion does not visit the rabbit then the lion does not like the rabbit. If the lion likes the rabbit and the rabbit does not see the lion then the rabbit visits the lion.
The lion is not big.
("lion" "is" "big" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone is big and they do not see the lion then the lion visits the rabbit.
((("someone" "is" "big" "+") ("someone" "sees" "lion" "~")) -> ("lion" "visits" "rabbit" "+"))
If the lion is nice and the lion does not visit the rabbit then the lion does not like the rabbit.
((("lion" "is" "nice" "+") ("lion" "visits" "rabbit" "~")) -> ("lion" "likes" "rabbit" "-"))
If the lion likes the rabbit and the rabbit does not see the lion then the rabbit visits the lion.
((("lion" "likes" "rabbit" "+") ("rabbit" "sees" "lion" "~")) -> ("rabbit" "visits" "lion" "+"))
The rabbit is rough.
True
1
proof
[(triple11)]
("rabbit" "is" "rough" "+")
triple11
The rabbit is not young.
False
1
inv-proof
[(triple12)]
("rabbit" "is" "young" "-")
triple12
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
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 is nice.[(triple2)] The lion is not big.[(triple1)] The lion is rough.[(triple3)] The lion is young.[(triple4)] The lion likes the rabbit.[(triple5)] The lion sees the rabbit.[(triple6)] The lion visits the rabbit.[(triple7)] The rabbit is blue.[(triple9)] The rabbit is nice.[(triple10)] The rabbit is not big.[(triple8)] The rabbit is rough.[(triple11)] The rabbit is young.[(triple12)] The rabbit likes the lion.[(triple13)] The rabbit sees the lion.[(triple14)] The rabbit visits the lion.[(triple15)]
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is not big.
("lion" "is" "big" "-")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple5
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple6
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit is not big.
("rabbit" "is" "big" "-")
triple8
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple13
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple14
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15