The rabbit is cold. The rabbit is kind. The rabbit is not nice. If something is kind and not nice then it is big.
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
If something is kind and not nice then it is big.
((("something" "is" "kind" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "+"))
The rabbit is not nice.
True
1
proof
[(triple3)]
("rabbit" "is" "nice" "-")
triple3
The rabbit is not kind.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "kind" "-")
triple2
The rabbit is big.
True
3
proof
[(((triple2 triple3) -> rule1))]
("rabbit" "is" "big" "+")
((triple2 triple3) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("rabbit" "is" "big" "-")
((triple2 triple3) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
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" "+")
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 blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The rabbit is cold.[(triple1)] The rabbit is kind.[(triple2)] The rabbit is not nice.[(triple3)] @1: The rabbit is big.[(((triple2 triple3) -> rule1))]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
((triple2 triple3) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1