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