The rabbit is green. If someone is green and not young then they are not rough. Nice people are rough. If someone is round and not young then they are rough. If someone is green then they are nice. All rough people are round. If the rabbit is nice and the rabbit is not young then the rabbit is round.
The rabbit is green.
("rabbit" "is" "green" "+")
If someone is green and not young then they are not rough.
((("someone" "is" "green" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "-"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is round and not young then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "+"))
If someone is green then they are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All rough people are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If the rabbit is nice and the rabbit is not young then the rabbit is round.
((("rabbit" "is" "nice" "+") ("rabbit" "is" "young" "~")) -> ("rabbit" "is" "round" "+"))
The rabbit is green.
True
1
proof
[(triple1)]
("rabbit" "is" "green" "+")
triple1
The rabbit is not green.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "green" "-")
triple1
The rabbit is nice.
True
2
proof
[(((triple1) -> rule4))]
("rabbit" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is not nice.
False
2
inv-proof
[(((triple1) -> rule4))]
("rabbit" "is" "nice" "-")
((triple1) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("rabbit" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("rabbit" "is" "rough" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit is not round.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "is" "round" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
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 is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
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 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)] @1: The rabbit is nice.[(((triple1) -> rule4))] @2: The rabbit is rough.[(((((triple1) -> rule4)) -> rule2))] @3: The rabbit is round.[(((((((triple1) -> rule4)) -> rule2)) -> rule5))]
The rabbit is green.
("rabbit" "is" "green" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple1) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3