The rabbit is not kind. The rabbit is nice. The rabbit is young. All young, green people are big. If someone is young and not kind then they are big. Kind people are young. If someone is kind and not nice then they are young. If the rabbit is nice then the rabbit is young. Nice people are green.
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
All young, green people are big.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is young and not kind then they are big.
((("someone" "is" "young" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "big" "+"))
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not nice then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "young" "+"))
If the rabbit is nice then the rabbit is young.
((("rabbit" "is" "nice" "+")) -> ("rabbit" "is" "young" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
The rabbit is nice.
True
1
proof
[(triple2)]
("rabbit" "is" "nice" "+")
triple2
The rabbit is not young.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule5))]
("rabbit" "is" "young" "-")
triple3
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is big.
True
3
proof
[(((triple3 triple1) -> rule2) OR ((triple3 ((triple2) -> rule6)) -> rule1) OR ((((triple2) -> rule5) triple1) -> rule2) OR ((((triple2) -> rule5) ((triple2) -> rule6)) -> rule1))]
("rabbit" "is" "big" "+")
((triple3 triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple2) -> (rule5 % int2)) triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The rabbit is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("rabbit" "is" "green" "-")
((triple2) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
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 nice.[(triple2)] The rabbit is not kind.[(triple1)] The rabbit is young.[(triple3 OR ((triple2) -> rule5))] @1: The rabbit is big.[(((triple3 triple1) -> rule2) OR ((triple3 ((triple2) -> rule6)) -> rule1) OR ((((triple2) -> rule5) triple1) -> rule2) OR ((((triple2) -> rule5) ((triple2) -> rule6)) -> rule1))] The rabbit is green.[(((triple2) -> rule6))]
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple1
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple3 triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((triple3 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple2) -> (rule5 % int2)) triple1) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
((triple2) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1