The lion is rough. The lion is round. The lion likes the mouse. The lion likes the rabbit. The mouse is round. The rabbit is round. The rabbit visits the lion. If someone visits the rabbit then they are big. If the rabbit is red then the rabbit is not rough.
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone visits the rabbit then they are big.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "big" "+"))
If the rabbit is red then the rabbit is not rough.
((("rabbit" "is" "red" "+")) -> ("rabbit" "is" "rough" "-"))
The lion likes the rabbit.
True
1
proof
[(triple4)]
("lion" "likes" "rabbit" "+")
triple4
The lion is not rough.
False
1
inv-proof
[(triple1)]
("lion" "is" "rough" "-")
triple1
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "big" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The lion is rough.[(triple1)] The lion is round.[(triple2)] The lion likes the mouse.[(triple3)] The lion likes the rabbit.[(triple4)] The mouse is round.[(triple5)] The rabbit is round.[(triple6)] The rabbit visits the lion.[(triple7)]
The lion is rough.
("lion" "is" "rough" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple7