The rabbit is nice. Nice people are kind. All blue people are kind. If someone is nice then they are kind. If the rabbit is nice and the rabbit is kind then the rabbit is round. If the rabbit is blue then the rabbit is big. Kind, big people are blue.
The rabbit is nice.
("rabbit" "is" "nice" "+")
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If the rabbit is nice and the rabbit is kind then the rabbit is round.
((("rabbit" "is" "nice" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit is blue then the rabbit is big.
((("rabbit" "is" "blue" "+")) -> ("rabbit" "is" "big" "+"))
Kind, big people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
The rabbit is nice.
True
1
proof
[(triple1)]
("rabbit" "is" "nice" "+")
triple1
The rabbit is not nice.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "nice" "-")
triple1
The rabbit is kind.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("rabbit" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("rabbit" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule4))]
("rabbit" "is" "round" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is not round.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule4))]
("rabbit" "is" "round" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is not big.
Unknown
inv-rconc
[@2: The rabbit is big.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("rabbit" "is" "big" "-")
The rabbit is blue.
Unknown
rconc
[@2: The rabbit is blue.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("rabbit" "is" "blue" "+")
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 nice.[(triple1)] @1: The rabbit is kind.[(((triple1) -> rule1) OR ((triple1) -> rule3))] @2: The rabbit is round.[(((triple1 ((triple1) -> rule1)) -> rule4) OR ((triple1 ((triple1) -> rule3)) -> rule4))]
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2