The cow chases the mouse. The cow eats the lion. The cow eats the mouse. The cow is young. The cow sees the lion. The cow sees the mouse. The lion eats the cow. The lion is not young. The mouse eats the cow. The mouse eats the lion. The mouse sees the cow. The mouse sees the lion. If something eats the mouse then the mouse does not chase the lion. If something chases the cow then it sees the mouse.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is not young.
("lion" "is" "young" "-")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something eats the mouse then the mouse does not chase the lion.
((("something" "eats" "mouse" "+")) -> ("mouse" "chases" "lion" "-"))
If something chases the cow then it sees the mouse.
((("something" "chases" "cow" "+")) -> ("something" "sees" "mouse" "+"))
The cow sees the mouse.
True
1
proof
[(triple6)]
("cow" "sees" "mouse" "+")
triple6
The cow does not eat the lion.
False
1
inv-proof
[(triple2)]
("cow" "eats" "lion" "-")
triple2
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cow chases the lion.
Unknown
random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "+")
@0: The cow chases the mouse.[(triple1)] The cow eats the lion.[(triple2)] The cow eats the mouse.[(triple3)] The cow is young.[(triple4)] The cow sees the lion.[(triple5)] The cow sees the mouse.[(triple6)] The lion eats the cow.[(triple7)] The lion is not young.[(triple8)] The mouse eats the cow.[(triple9)] The mouse eats the lion.[(triple10)] The mouse sees the cow.[(triple11)] The mouse sees the lion.[(triple12)] @1: The mouse does not chase the lion.[(((triple3) -> rule1))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow eats the lion.
("cow" "eats" "lion" "+")
triple2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The lion eats the cow.
("lion" "eats" "cow" "+")
triple7
The lion is not young.
("lion" "is" "young" "-")
triple8
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple9
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple12
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
((triple3) -> (rule1 % int1))
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int1