The rabbit is rough. If the rabbit is rough then the rabbit is round. If something is kind then it is rough. If the rabbit is nice and the rabbit is round then the rabbit is blue. Kind things are nice. If the rabbit is round then the rabbit is nice. Nice things are rough.
The rabbit is rough.
("rabbit" "is" "rough" "+")
If the rabbit is rough then the rabbit is round.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "round" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If the rabbit is nice and the rabbit is round then the rabbit is blue.
((("rabbit" "is" "nice" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "is" "blue" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If the rabbit is round then the rabbit is nice.
((("rabbit" "is" "round" "+")) -> ("rabbit" "is" "nice" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
The rabbit is rough.
True
1
proof
[(triple1)]
("rabbit" "is" "rough" "+")
triple1
The rabbit is not rough.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "rough" "-")
triple1
The rabbit is round.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "-")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is blue.
True
6
proof
[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule3))]
("rabbit" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is not blue.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule3))]
("rabbit" "is" "blue" "-")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
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 rough.[(triple1)] @1: The rabbit is round.[(((triple1) -> rule1))] @2: The rabbit is nice.[(((((triple1) -> rule1)) -> rule5))] @3: The rabbit is blue.[(((((((triple1) -> rule1)) -> rule5) ((triple1) -> rule1)) -> rule3))]
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3