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