The lion visits the rabbit. The rabbit visits the lion. If something visits the lion then it is nice. If something sees the rabbit then it sees the lion. If something is rough then it visits the rabbit. If something visits the rabbit and the rabbit is rough then the rabbit is big. If the rabbit is rough and the rabbit needs the lion then the rabbit visits the lion. If something needs the rabbit and the rabbit sees the lion then it is nice. All kind things are nice. If something needs the rabbit and the rabbit is rough then the rabbit is big.
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If something visits the lion then it is nice.
((("something" "visits" "lion" "+")) -> ("something" "is" "nice" "+"))
If something sees the rabbit then it sees the lion.
((("something" "sees" "rabbit" "+")) -> ("something" "sees" "lion" "+"))
If something is rough then it visits the rabbit.
((("something" "is" "rough" "+")) -> ("something" "visits" "rabbit" "+"))
If something visits the rabbit and the rabbit is rough then the rabbit is big.
((("something" "visits" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "big" "+"))
If the rabbit is rough and the rabbit needs the lion then the rabbit visits the lion.
((("rabbit" "is" "rough" "+") ("rabbit" "needs" "lion" "+")) -> ("rabbit" "visits" "lion" "+"))
If something needs the rabbit and the rabbit sees the lion then it is nice.
((("something" "needs" "rabbit" "+") ("rabbit" "sees" "lion" "+")) -> ("something" "is" "nice" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something needs the rabbit and the rabbit is rough then the rabbit is big.
((("something" "needs" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "big" "+"))
The lion visits the rabbit.
True
1
proof
[(triple1)]
("lion" "visits" "rabbit" "+")
triple1
The lion does not visit the rabbit.
False
1
inv-proof
[(triple1)]
("lion" "visits" "rabbit" "-")
triple1
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "lion" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The lion visits the rabbit.[(triple1)] The rabbit visits the lion.[(triple2)] @1: The rabbit is nice.[(((triple2) -> rule1))]
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1