The rabbit is round. If the rabbit is green then the rabbit is not red. Round, nice things are not green. If something is round then it is nice.
The rabbit is round.
("rabbit" "is" "round" "+")
If the rabbit is green then the rabbit is not red.
((("rabbit" "is" "green" "+")) -> ("rabbit" "is" "red" "-"))
Round, nice things are not green.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
If something is round then it is nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
The rabbit is round.
True
1
proof
[(triple1)]
("rabbit" "is" "round" "+")
triple1
The rabbit is not round.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "round" "-")
triple1
The rabbit is nice.
True
2
proof
[(((triple1) -> rule3))]
("rabbit" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("rabbit" "is" "nice" "-")
((triple1) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not green.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("rabbit" "is" "green" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("rabbit" "is" "green" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "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 chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The rabbit is round.[(triple1)] @1: The rabbit is nice.[(((triple1) -> rule3))] @2: The rabbit is not green.[(((triple1 ((triple1) -> rule3)) -> rule2))]
The rabbit is round.
("rabbit" "is" "round" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not green.
("rabbit" "is" "green" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2