The rabbit is young. The squirrel likes the rabbit. If someone likes the squirrel and they see the squirrel then they are green. If someone likes the rabbit then they are kind. If the squirrel is kind then the squirrel is round.
The rabbit is young.
("rabbit" "is" "young" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If someone likes the squirrel and they see the squirrel then they are green.
((("someone" "likes" "squirrel" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "is" "green" "+"))
If someone likes the rabbit then they are kind.
((("someone" "likes" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
If the squirrel is kind then the squirrel is round.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "round" "+"))
The rabbit is young.
True
1
proof
[(triple1)]
("rabbit" "is" "young" "+")
triple1
The squirrel does not like the rabbit.
False
1
inv-proof
[(triple2)]
("squirrel" "likes" "rabbit" "-")
triple2
The squirrel is kind.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "is" "kind" "+")
((triple2) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "is" "kind" "-")
((triple2) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is round.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("squirrel" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("squirrel" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "-")
The rabbit is kind.
Unknown
rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "kind" "+")
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "green" "-")
The rabbit eats the squirrel.
Unknown
random
[@0: The rabbit eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The rabbit is young.[(triple1)] The squirrel likes the rabbit.[(triple2)] @1: The squirrel is kind.[(((triple2) -> rule2))] @2: The squirrel is round.[(((((triple2) -> rule2)) -> rule3))]
The rabbit is young.
("rabbit" "is" "young" "+")
triple1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple2) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2