The rabbit is kind. The rabbit is not nice. The rabbit is round. If something is young and nice then it is not round. If something is nice and big then it is kind. If the rabbit is round and the rabbit is young then the rabbit is nice.
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
If something is young and nice then it is not round.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "-"))
If something is nice and big then it is kind.
((("something" "is" "nice" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If the rabbit is round and the rabbit is young then the rabbit is nice.
((("rabbit" "is" "round" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "is" "nice" "+"))
The rabbit is kind.
True
1
proof
[(triple1)]
("rabbit" "is" "kind" "+")
triple1
The rabbit is nice.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "nice" "+")
triple2
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
@0: The rabbit is kind.[(triple1)] The rabbit is not nice.[(triple2)] The rabbit is round.[(triple3)]
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple1
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3