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