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