The cow needs the lion. The lion sees the mouse. The mouse eats the cow. The rabbit does not need the lion. If something eats the lion and the lion does not need the rabbit then the lion needs the mouse. If the rabbit is rough and the rabbit is not blue then the rabbit does not eat the mouse. If something eats the mouse and it does not eat the rabbit then the rabbit is not rough. If something needs the rabbit and it eats the cow then the cow does not need the mouse. If something sees the cow then it needs the mouse. If something eats the cow then it sees the cow. If something needs the mouse then the mouse eats the lion. If something is rough and it needs the rabbit then the rabbit is red.
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
If something eats the lion and the lion does not need the rabbit then the lion needs the mouse.
((("something" "eats" "lion" "+") ("lion" "needs" "rabbit" "~")) -> ("lion" "needs" "mouse" "+"))
If the rabbit is rough and the rabbit is not blue then the rabbit does not eat the mouse.
((("rabbit" "is" "rough" "+") ("rabbit" "is" "blue" "~")) -> ("rabbit" "eats" "mouse" "-"))
If something eats the mouse and it does not eat the rabbit then the rabbit is not rough.
((("something" "eats" "mouse" "+") ("something" "eats" "rabbit" "~")) -> ("rabbit" "is" "rough" "-"))
If something needs the rabbit and it eats the cow then the cow does not need the mouse.
((("something" "needs" "rabbit" "+") ("something" "eats" "cow" "+")) -> ("cow" "needs" "mouse" "-"))
If something sees the cow then it needs the mouse.
((("something" "sees" "cow" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the cow then it sees the cow.
((("something" "eats" "cow" "+")) -> ("something" "sees" "cow" "+"))
If something needs the mouse then the mouse eats the lion.
((("something" "needs" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If something is rough and it needs the rabbit then the rabbit is red.
((("something" "is" "rough" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
The cow needs the lion.
True
1
proof
[(triple1)]
("cow" "needs" "lion" "+")
triple1
The lion does not see the mouse.
False
1
inv-proof
[(triple2)]
("lion" "sees" "mouse" "-")
triple2
The mouse sees the cow.
True
2
proof
[(((triple3) -> rule6))]
("mouse" "sees" "cow" "+")
((triple3) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse does not see the cow.
False
2
inv-proof
[(((triple3) -> rule6))]
("mouse" "sees" "cow" "-")
((triple3) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("mouse" "needs" "mouse" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The rabbit does not see the cow.
Unknown
inv-rconc
[@1: The rabbit sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "cow" "-")
The rabbit is red.
Unknown
rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "red" "+")
The rabbit does not need the mouse.
Unknown
inv-rconc
[@2: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The rabbit does not see the mouse.
Unknown
inv-random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "-")
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 needs the lion.[(triple1)] The lion sees the mouse.[(triple2)] The mouse eats the cow.[(triple3)] The rabbit does not need the lion.[(triple4)] @1: The mouse sees the cow.[(((triple3) -> rule6))] @2: The mouse needs the mouse.[(((((triple3) -> rule6)) -> rule5))] @3: The mouse eats the lion.[(((((((triple3) -> rule6)) -> rule5)) -> rule7))]
The cow needs the lion.
("cow" "needs" "lion" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple3
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple4
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple3) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3