The rabbit is kind. The rabbit is not round. The rabbit is not young. If someone is round then they are big. Kind people are big. All big people are not round. If the rabbit is big and the rabbit is round then the rabbit is young. If the rabbit is kind then the rabbit is not round. If someone is round and not big then they are young. If the rabbit is young and the rabbit is not round then the rabbit is not red. If someone is young then they are red.
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit is not young.
("rabbit" "is" "young" "-")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
All big people are not round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "-"))
If the rabbit is big and the rabbit is round then the rabbit is young.
((("rabbit" "is" "big" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "is" "young" "+"))
If the rabbit is kind then the rabbit is not round.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "round" "-"))
If someone is round and not big then they are young.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "young" "+"))
If the rabbit is young and the rabbit is not round then the rabbit is not red.
((("rabbit" "is" "young" "+") ("rabbit" "is" "round" "~")) -> ("rabbit" "is" "red" "-"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
The rabbit is kind.
True
1
proof
[(triple1)]
("rabbit" "is" "kind" "+")
triple1
The rabbit is young.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "young" "+")
triple3
The rabbit is big.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "is" "big" "+")
((triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "is" "big" "-")
((triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "red" "-")
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 visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is kind.[(triple1)] The rabbit is not round.[(triple2 OR ((triple1) -> rule5) OR ((((triple1) -> rule2)) -> rule3))] The rabbit is not young.[(triple3)] @1: The rabbit is big.[(((triple1) -> rule2))]
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple1
The rabbit is not round.
("rabbit" "is" "round" "-")
triple2
((triple1) -> (rule5 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not young.
("rabbit" "is" "young" "-")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
((triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1