The bear chases the cow. The cow sees the rabbit. The mouse sees the rabbit. The rabbit sees the bear. If someone sees the mouse then the mouse likes the bear. If someone sees the mouse then the mouse likes the cow. If someone sees the rabbit then the rabbit does not chase the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If someone sees the mouse then the mouse likes the bear.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If someone sees the mouse then the mouse likes the cow.
((("someone" "sees" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If someone sees the rabbit then the rabbit does not chase the bear.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "bear" "-"))
The mouse sees the rabbit.
True
1
proof
[(triple3)]
("mouse" "sees" "rabbit" "+")
triple3
The cow does not see the rabbit.
False
1
inv-proof
[(triple2)]
("cow" "sees" "rabbit" "-")
triple2
The rabbit does not chase the bear.
True
2
proof
[(((triple2) -> rule3) OR ((triple3) -> rule3))]
("rabbit" "chases" "bear" "-")
((triple2) -> (rule3 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1
((triple3) -> (rule3 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1
The rabbit chases the bear.
False
2
inv-proof
[(((triple2) -> rule3) OR ((triple3) -> rule3))]
("rabbit" "chases" "bear" "+")
((triple2) -> (rule3 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1
((triple3) -> (rule3 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1
The mouse does not like the bear.
Unknown
inv-rconc
[@1: The mouse likes the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "bear" "-")
The mouse likes the cow.
Unknown
rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "cow" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
@0: The bear chases the cow.[(triple1)] The cow sees the rabbit.[(triple2)] The mouse sees the rabbit.[(triple3)] The rabbit sees the bear.[(triple4)] @1: The rabbit does not chase the bear.[(((triple2) -> rule3) OR ((triple3) -> rule3))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple3
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple4
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
((triple2) -> (rule3 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1
((triple3) -> (rule3 % int1))
The rabbit does not chase the bear.
("rabbit" "chases" "bear" "-")
int1