The cow sees the rabbit. The mouse likes the rabbit. The rabbit is cold. If someone likes the mouse then the mouse is kind. If someone sees the rabbit and they see the cow then they need the cow. If someone is green then they do not need the cow. If someone is blue then they need the rabbit. If someone is nice and they do not like the cow then they are kind. If someone sees the rabbit then the rabbit is blue. If someone needs the mouse and they see the rabbit then they are nice. If someone needs the rabbit then they like the mouse.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
If someone likes the mouse then the mouse is kind.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If someone sees the rabbit and they see the cow then they need the cow.
((("someone" "sees" "rabbit" "+") ("someone" "sees" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone is green then they do not need the cow.
((("someone" "is" "green" "+")) -> ("someone" "needs" "cow" "-"))
If someone is blue then they need the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is nice and they do not like the cow then they are kind.
((("someone" "is" "nice" "+") ("someone" "likes" "cow" "~")) -> ("someone" "is" "kind" "+"))
If someone sees the rabbit then the rabbit is blue.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If someone needs the mouse and they see the rabbit then they are nice.
((("someone" "needs" "mouse" "+") ("someone" "sees" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the rabbit then they like the mouse.
((("someone" "needs" "rabbit" "+")) -> ("someone" "likes" "mouse" "+"))
The mouse likes the rabbit.
True
1
proof
[(triple2)]
("mouse" "likes" "rabbit" "+")
triple2
The mouse does not like the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "likes" "rabbit" "-")
triple2
The rabbit is blue.
True
2
proof
[(((triple1) -> rule6))]
("rabbit" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("rabbit" "is" "blue" "-")
((triple1) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit needs the rabbit.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("rabbit" "needs" "rabbit" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit does not need the rabbit.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("rabbit" "needs" "rabbit" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the mouse.
True
4
proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule8))]
("rabbit" "likes" "mouse" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit does not like the mouse.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule4)) -> rule8))]
("rabbit" "likes" "mouse" "-")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "kind" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "nice" "+")
The cow does not like the mouse.
Unknown
inv-rconc
[@2: The cow likes the mouse.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("cow" "likes" "mouse" "-")
The mouse needs the cow.
Unknown
rconc
[@1: The mouse needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "cow" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The rabbit sees the mouse.
Unknown
random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "+")
@0: The cow sees the rabbit.[(triple1)] The mouse likes the rabbit.[(triple2)] The rabbit is cold.[(triple3)] @1: The rabbit is blue.[(((triple1) -> rule6))] @2: The rabbit needs the rabbit.[(((((triple1) -> rule6)) -> rule4))] @3: The rabbit likes the mouse.[(((((((triple1) -> rule6)) -> rule4)) -> rule8))] @4: The mouse is kind.[(((((((((triple1) -> rule6)) -> rule4)) -> rule8)) -> rule1))]
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple2
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
((((((((triple1) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is blue.
("rabbit" "is" "blue" "+")
int4