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