The rabbit is blue. The rabbit is green. The rabbit is kind. The rabbit is nice. The rabbit is rough. If something is kind then it is rough. If something is green and kind then it is nice. All kind things are nice. All rough, blue things are nice. If something is kind and rough then it is green. If something is rough and kind then it is nice.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is green and kind then it is nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All rough, blue things are nice.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is kind and rough then it is green.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is rough and kind then it is nice.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
The rabbit is rough.
True
1
proof
[(triple5 OR ((triple3) -> rule1))]
("rabbit" "is" "rough" "+")
triple5
((triple3) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is not kind.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
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 eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The rabbit is blue.[(triple1)] The rabbit is green.[(triple2 OR ((triple3 triple5) -> rule5) OR ((triple3 ((triple3) -> rule1)) -> rule5))] The rabbit is kind.[(triple3)] The rabbit is nice.[(triple4 OR ((triple3) -> rule3) OR ((triple2 triple3) -> rule2) OR ((triple5 triple1) -> rule4) OR ((triple5 triple3) -> rule6) OR ((((triple3) -> rule1) triple1) -> rule4) OR ((((triple3) -> rule1) triple3) -> rule6) OR ((((triple3 triple5) -> rule5) triple3) -> rule2) OR ((((triple3 ((triple3) -> rule1)) -> rule5) triple3) -> rule2))] The rabbit is rough.[(triple5 OR ((triple3) -> rule1))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
((triple3 triple5) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
((triple3) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple2 triple3) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple5 triple1) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple5 triple3) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((((triple3) -> (rule1 % int2)) triple3) -> (rule6 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
((((triple3 triple5) -> (rule5 % int2)) triple3) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple3) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
((triple3) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1