The cow is red. The lion is blue. The mouse is cold. The rabbit is big. Big things are blue. If the cow is blue and the cow is red then the cow eats the rabbit. If something eats the rabbit then the rabbit sees the mouse. If something likes the lion and it likes the cow then the cow sees the mouse. If the lion likes the mouse then the mouse eats the cow. If something eats the cow and it likes the lion then the lion eats the cow. If something sees the cow and the cow is cold then it eats the mouse. If something likes the cow and it eats the mouse then the mouse sees the cow.
The cow is red.
("cow" "is" "red" "+")
The lion is blue.
("lion" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If the cow is blue and the cow is red then the cow eats the rabbit.
((("cow" "is" "blue" "+") ("cow" "is" "red" "+")) -> ("cow" "eats" "rabbit" "+"))
If something eats the rabbit then the rabbit sees the mouse.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something likes the lion and it likes the cow then the cow sees the mouse.
((("something" "likes" "lion" "+") ("something" "likes" "cow" "+")) -> ("cow" "sees" "mouse" "+"))
If the lion likes the mouse then the mouse eats the cow.
((("lion" "likes" "mouse" "+")) -> ("mouse" "eats" "cow" "+"))
If something eats the cow and it likes the lion then the lion eats the cow.
((("something" "eats" "cow" "+") ("something" "likes" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If something sees the cow and the cow is cold then it eats the mouse.
((("something" "sees" "cow" "+") ("cow" "is" "cold" "+")) -> ("something" "eats" "mouse" "+"))
If something likes the cow and it eats the mouse then the mouse sees the cow.
((("something" "likes" "cow" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
The mouse is cold.
True
1
proof
[(triple3)]
("mouse" "is" "cold" "+")
triple3
The lion is not blue.
False
1
inv-proof
[(triple2)]
("lion" "is" "blue" "-")
triple2
The lion does not eat the mouse.
Unknown
inv-rconc
[@1: The lion eats the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "eats" "mouse" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
@0: The cow is red.[(triple1)] The lion is blue.[(triple2)] The mouse is cold.[(triple3)] The rabbit is big.[(triple4)] @1: The rabbit is blue.[(((triple4) -> rule1))]
The cow is red.
("cow" "is" "red" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple4) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1