The rabbit is kind. All big, round people are cold. If someone is red and not kind then they are cold. If someone is kind and big then they are red. All red people are round. If the rabbit is cold then the rabbit is round. If the rabbit is kind then the rabbit is red. If the rabbit is round and the rabbit is kind then the rabbit is cold. If someone is round and not kind then they are not big.
The rabbit is kind.
("rabbit" "is" "kind" "+")
All big, round people are cold.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is red and not kind then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "cold" "+"))
If someone is kind and big then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If the rabbit is cold then the rabbit is round.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit is kind then the rabbit is red.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "red" "+"))
If the rabbit is round and the rabbit is kind then the rabbit is cold.
((("rabbit" "is" "round" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is round and not kind then they are not big.
((("someone" "is" "round" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "big" "-"))
The rabbit is kind.
True
1
proof
[(triple1)]
("rabbit" "is" "kind" "+")
triple1
The rabbit is not kind.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "kind" "-")
triple1
The rabbit is red.
True
2
proof
[(((triple1) -> rule6))]
("rabbit" "is" "red" "+")
((triple1) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple1) -> rule6))]
("rabbit" "is" "red" "-")
((triple1) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("rabbit" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("rabbit" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is cold.
True
5
proof
[(((((((triple1) -> rule6)) -> rule4) triple1) -> rule7))]
("rabbit" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit is not cold.
False
5
inv-proof
[(((((((triple1) -> rule6)) -> rule4) triple1) -> rule7))]
("rabbit" "is" "cold" "-")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
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 visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The rabbit is kind.[(triple1)] @1: The rabbit is red.[(((triple1) -> rule6))] @2: The rabbit is round.[(((((triple1) -> rule6)) -> rule4))] @3: The rabbit is cold.[(((((((triple1) -> rule6)) -> rule4) triple1) -> rule7))]
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3