The rabbit is round. All round people are red. Round, big people are red. If someone is nice then they are red. If someone is nice then they are red. If the rabbit is rough then the rabbit is round. If someone is rough then they are big. Red, round people are big. If someone is red and round then they are not nice.
The rabbit is round.
("rabbit" "is" "round" "+")
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
Round, big people are red.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If the rabbit is rough then the rabbit is round.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "round" "+"))
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Red, round people are big.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is red and round then they are not nice.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "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 red.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "red" "+")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "red" "-")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not nice.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule8))]
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not big.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule7))]
("rabbit" "is" "big" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit is round.[(triple1)] @1: The rabbit is red.[(((triple1) -> rule1))] @2: The rabbit is big.[(((((triple1) -> rule1) triple1) -> rule7))] The rabbit is not nice.[(((((triple1) -> rule1) triple1) -> rule8))]
The rabbit is round.
("rabbit" "is" "round" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not nice.
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule8 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2