The rabbit is big. The rabbit is blue. The rabbit is kind. If something is big then it is kind. If the rabbit is nice and the rabbit is green then the rabbit is kind. If something is green then it is blue.
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If the rabbit is nice and the rabbit is green then the rabbit is kind.
((("rabbit" "is" "nice" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "is" "kind" "+"))
If something is green then it is blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
The rabbit is kind.
True
1
proof
[(triple3 OR ((triple1) -> rule1))]
("rabbit" "is" "kind" "+")
triple3
((triple1) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not blue.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "blue" "-")
triple2
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is big.[(triple1)] The rabbit is blue.[(triple2)] The rabbit is kind.[(triple3 OR ((triple1) -> rule1))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
((triple1) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1