The cow eats the lion. The cow eats the mouse. The cow likes the mouse. The lion eats the rabbit. The lion is green. The mouse is red. The mouse likes the lion. The mouse needs the lion. The rabbit is blue. The rabbit needs the lion. If something eats the cow and it does not like the rabbit then the cow eats the mouse. If something is blue then it likes the cow. If something likes the rabbit and the rabbit is green then the rabbit eats the mouse. If something eats the mouse and the mouse is young then the mouse needs the rabbit. If something is young and it likes the cow then it is red. If something is green and it does not like the cow then the cow is red.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is green.
("lion" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If something eats the cow and it does not like the rabbit then the cow eats the mouse.
((("something" "eats" "cow" "+") ("something" "likes" "rabbit" "~")) -> ("cow" "eats" "mouse" "+"))
If something is blue then it likes the cow.
((("something" "is" "blue" "+")) -> ("something" "likes" "cow" "+"))
If something likes the rabbit and the rabbit is green then the rabbit eats the mouse.
((("something" "likes" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "eats" "mouse" "+"))
If something eats the mouse and the mouse is young then the mouse needs the rabbit.
((("something" "eats" "mouse" "+") ("mouse" "is" "young" "+")) -> ("mouse" "needs" "rabbit" "+"))
If something is young and it likes the cow then it is red.
((("something" "is" "young" "+") ("something" "likes" "cow" "+")) -> ("something" "is" "red" "+"))
If something is green and it does not like the cow then the cow is red.
((("something" "is" "green" "+") ("something" "likes" "cow" "~")) -> ("cow" "is" "red" "+"))
The mouse likes the lion.
True
1
proof
[(triple7)]
("mouse" "likes" "lion" "+")
triple7
The lion does not eat the rabbit.
False
1
inv-proof
[(triple4)]
("lion" "eats" "rabbit" "-")
triple4
The rabbit likes the cow.
True
2
proof
[(((triple9) -> rule2))]
("rabbit" "likes" "cow" "+")
((triple9) -> (rule2 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The rabbit does not like the cow.
False
2
inv-proof
[(((triple9) -> rule2))]
("rabbit" "likes" "cow" "-")
((triple9) -> (rule2 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1
The rabbit does not eat the mouse.
Unknown
inv-rconc
[@1: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "mouse" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "red" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion eats the mouse.
Unknown
random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "+")
@0: The cow eats the lion.[(triple1)] The cow eats the mouse.[(triple2)] The cow likes the mouse.[(triple3)] The lion eats the rabbit.[(triple4)] The lion is green.[(triple5)] The mouse is red.[(triple6)] The mouse likes the lion.[(triple7)] The mouse needs the lion.[(triple8)] The rabbit is blue.[(triple9)] The rabbit needs the lion.[(triple10)] @1: The rabbit likes the cow.[(((triple9) -> rule2))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple7
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple10
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
((triple9) -> (rule2 % int1))
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
int1