The rabbit is blue. The rabbit is nice. The rabbit is young. All nice, blue things are rough. If the rabbit is young and the rabbit is kind then the rabbit is nice. All blue, young things are nice.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
All nice, blue things are rough.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If the rabbit is young and the rabbit is kind then the rabbit is nice.
((("rabbit" "is" "young" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "nice" "+"))
All blue, young things are nice.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
The rabbit is nice.
True
1
proof
[(triple2 OR ((triple1 triple3) -> rule3))]
("rabbit" "is" "nice" "+")
triple2
((triple1 triple3) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not blue.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "blue" "-")
triple1
The rabbit is rough.
True
3
proof
[(((triple2 triple1) -> rule1) OR ((((triple1 triple3) -> rule3) triple1) -> rule1))]
("rabbit" "is" "rough" "+")
((triple2 triple1) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
((((triple1 triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((triple2 triple1) -> rule1) OR ((((triple1 triple3) -> rule3) triple1) -> rule1))]
("rabbit" "is" "rough" "-")
((triple2 triple1) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
((((triple1 triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
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 visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The rabbit is blue.[(triple1)] The rabbit is nice.[(triple2 OR ((triple1 triple3) -> rule3))] The rabbit is young.[(triple3)] @1: The rabbit is rough.[(((triple2 triple1) -> rule1) OR ((((triple1 triple3) -> rule3) triple1) -> rule1))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
((triple1 triple3) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple2 triple1) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
((((triple1 triple3) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2