The cow sees the rabbit. The mouse eats the rabbit. The rabbit is not kind. If something sees the cow and it chases the mouse then it chases the cow. If something sees the cow and it eats the cow then the cow sees the mouse. If something is red and it chases the cow then it is not kind. If the cow sees the rabbit then the rabbit eats the cow. If the rabbit sees the cow and the rabbit chases the cow then the rabbit is red. If something sees the rabbit then the rabbit does not see the cow.
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
If something sees the cow and it chases the mouse then it chases the cow.
((("something" "sees" "cow" "+") ("something" "chases" "mouse" "+")) -> ("something" "chases" "cow" "+"))
If something sees the cow and it eats the cow then the cow sees the mouse.
((("something" "sees" "cow" "+") ("something" "eats" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If something is red and it chases the cow then it is not kind.
((("something" "is" "red" "+") ("something" "chases" "cow" "+")) -> ("something" "is" "kind" "-"))
If the cow sees the rabbit then the rabbit eats the cow.
((("cow" "sees" "rabbit" "+")) -> ("rabbit" "eats" "cow" "+"))
If the rabbit sees the cow and the rabbit chases the cow then the rabbit is red.
((("rabbit" "sees" "cow" "+") ("rabbit" "chases" "cow" "+")) -> ("rabbit" "is" "red" "+"))
If something sees the rabbit then the rabbit does not see the cow.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cow" "-"))
The rabbit is not kind.
True
1
proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "rabbit" "-")
triple2
The rabbit does not see the cow.
True
2
proof
[(((triple1) -> rule6))]
("rabbit" "sees" "cow" "-")
((triple1) -> (rule6 % int1))
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
int1
The rabbit does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule4))]
("rabbit" "eats" "cow" "-")
((triple1) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "red" "-")
The rabbit chases the cow.
Unknown
rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "cow" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow eats the mouse.
Unknown
random
[@0: The cow eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "mouse" "+")
@0: The cow sees the rabbit.[(triple1)] The mouse eats the rabbit.[(triple2)] The rabbit is not kind.[(triple3)] @1: The rabbit does not see the cow.[(((triple1) -> rule6))] The rabbit eats the cow.[(((triple1) -> rule4))]
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple2
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple3
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
((triple1) -> (rule6 % int1))
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((triple1) -> (rule4 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1