The bear needs the cow. The cow chases the mouse. The lion chases the cow. The lion is nice. The lion likes the bear. The lion likes the cow. The lion likes the mouse. The lion needs the mouse. The mouse chases the lion. The mouse is blue. The mouse is cold. The mouse likes the bear. If someone is nice then they need the bear. If someone is young and they need the bear then the bear likes the lion. If someone needs the cow and they like the bear then the bear chases the cow.
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
If someone is nice then they need the bear.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "bear" "+"))
If someone is young and they need the bear then the bear likes the lion.
((("someone" "is" "young" "+") ("someone" "needs" "bear" "+")) -> ("bear" "likes" "lion" "+"))
If someone needs the cow and they like the bear then the bear chases the cow.
((("someone" "needs" "cow" "+") ("someone" "likes" "bear" "+")) -> ("bear" "chases" "cow" "+"))
The lion likes the mouse.
True
1
proof
[(triple7)]
("lion" "likes" "mouse" "+")
triple7
The cow does not chase the mouse.
False
1
inv-proof
[(triple2)]
("cow" "chases" "mouse" "-")
triple2
The lion needs the bear.
True
2
proof
[(((triple4) -> rule1))]
("lion" "needs" "bear" "+")
((triple4) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion does not need the bear.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "needs" "bear" "-")
((triple4) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "needs" "bear" "-")
The bear likes the lion.
Unknown
rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "lion" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear needs the cow.[(triple1)] The cow chases the mouse.[(triple2)] The lion chases the cow.[(triple3)] The lion is nice.[(triple4)] The lion likes the bear.[(triple5)] The lion likes the cow.[(triple6)] The lion likes the mouse.[(triple7)] The lion needs the mouse.[(triple8)] The mouse chases the lion.[(triple9)] The mouse is blue.[(triple10)] The mouse is cold.[(triple11)] The mouse likes the bear.[(triple12)] @1: The lion needs the bear.[(((triple4) -> rule1))]
The bear needs the cow.
("bear" "needs" "cow" "+")
triple1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion likes the bear.
("lion" "likes" "bear" "+")
triple5
The lion likes the cow.
("lion" "likes" "cow" "+")
triple6
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple7
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple8
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple12
The lion needs the bear.
("lion" "needs" "bear" "+")
((triple4) -> (rule1 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1