The lion chases the rabbit. The lion is big. The lion visits the rabbit. The rabbit is big. The rabbit is kind. The rabbit does not visit the lion. The tiger is not big. If the rabbit does not like the tiger and the tiger does not visit the lion then the lion does not chase the tiger.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit does not visit the lion.
("rabbit" "visits" "lion" "-")
The tiger is not big.
("tiger" "is" "big" "-")
If the rabbit does not like the tiger and the tiger does not visit the lion then the lion does not chase the tiger.
((("rabbit" "likes" "tiger" "~") ("tiger" "visits" "lion" "~")) -> ("lion" "chases" "tiger" "-"))
The lion chases the rabbit.
True
1
proof
[(triple1)]
("lion" "chases" "rabbit" "+")
triple1
The lion is not big.
False
1
inv-proof
[(triple2)]
("lion" "is" "big" "-")
triple2
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit chases the tiger.
Unknown
random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is big.[(triple2)] The lion visits the rabbit.[(triple3)] The rabbit does not visit the lion.[(triple6)] The rabbit is big.[(triple4)] The rabbit is kind.[(triple5)] The tiger is not big.[(triple7)]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple3
The rabbit does not visit the lion.
("rabbit" "visits" "lion" "-")
triple6
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The tiger is not big.
("tiger" "is" "big" "-")
triple7