The rabbit is cold. If someone is cold then they are round. Round people are nice. If someone is red and not round then they are not blue.
The rabbit is cold.
("rabbit" "is" "cold" "+")
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and not round then they are not blue.
((("someone" "is" "red" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "blue" "-"))
The rabbit is cold.
True
1
proof
[(triple1)]
("rabbit" "is" "cold" "+")
triple1
The rabbit is not cold.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "cold" "-")
triple1
The rabbit is round.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "-")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
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 red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "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)] @1: The rabbit is round.[(((triple1) -> rule1))] @2: The rabbit is nice.[(((((triple1) -> rule1)) -> rule2))]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2