The bear is cold. The bear is young. The cow eats the mouse. The cow is cold. The cow needs the mouse. The lion is not red. The lion is round. The lion likes the mouse. The lion does not need the bear. The lion needs the cow. The mouse eats the cow. The mouse eats the lion. The mouse is young. The mouse likes the lion. The mouse needs the cow. If something eats the lion and the lion is young then it needs the mouse. If something eats the cow and it likes the bear then the bear is red. If something eats the bear then the bear is not red. If the lion likes the mouse then the lion is cold. If something likes the cow and the cow needs the lion then the lion needs the bear. If something likes the mouse and it is round then it eats the bear. If something is young and not big then it does not need the cow. If something eats the cow and the cow needs the lion then the cow is not round.
The bear is cold.
("bear" "is" "cold" "+")
The bear is young.
("bear" "is" "young" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The lion is not red.
("lion" "is" "red" "-")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
If something eats the lion and the lion is young then it needs the mouse.
((("something" "eats" "lion" "+") ("lion" "is" "young" "+")) -> ("something" "needs" "mouse" "+"))
If something eats the cow and it likes the bear then the bear is red.
((("something" "eats" "cow" "+") ("something" "likes" "bear" "+")) -> ("bear" "is" "red" "+"))
If something eats the bear then the bear is not red.
((("something" "eats" "bear" "+")) -> ("bear" "is" "red" "-"))
If the lion likes the mouse then the lion is cold.
((("lion" "likes" "mouse" "+")) -> ("lion" "is" "cold" "+"))
If something likes the cow and the cow needs the lion then the lion needs the bear.
((("something" "likes" "cow" "+") ("cow" "needs" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something likes the mouse and it is round then it eats the bear.
((("something" "likes" "mouse" "+") ("something" "is" "round" "+")) -> ("something" "eats" "bear" "+"))
If something is young and not big then it does not need the cow.
((("something" "is" "young" "+") ("something" "is" "big" "~")) -> ("something" "needs" "cow" "-"))
If something eats the cow and the cow needs the lion then the cow is not round.
((("something" "eats" "cow" "+") ("cow" "needs" "lion" "+")) -> ("cow" "is" "round" "-"))
The lion does not need the bear.
True
1
proof
[(triple9)]
("lion" "needs" "bear" "-")
triple9
The mouse does not like the lion.
False
1
inv-proof
[(triple14)]
("mouse" "likes" "lion" "-")
triple14
The lion does not need the mouse.
Unknown
inv-rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "mouse" "-")
The bear likes the cow.
Unknown
random
[@0: The bear likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cow" "+")
@0: The bear is cold.[(triple1)] The bear is young.[(triple2)] The cow eats the mouse.[(triple3)] The cow is cold.[(triple4)] The cow needs the mouse.[(triple5)] The lion does not need the bear.[(triple9)] The lion is not red.[(triple6)] The lion is round.[(triple7)] The lion likes the mouse.[(triple8)] The lion needs the cow.[(triple10)] The mouse eats the cow.[(triple11)] The mouse eats the lion.[(triple12)] The mouse is young.[(triple13)] The mouse likes the lion.[(triple14)] The mouse needs the cow.[(triple15)] @1: The lion eats the bear.[(((triple8 triple7) -> rule6))] The lion is cold.[(((triple8) -> rule4))] @2: The bear is not red.[(((((triple8 triple7) -> rule6)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple5
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple9
The lion is not red.
("lion" "is" "red" "-")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple8
The lion needs the cow.
("lion" "needs" "cow" "+")
triple10
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple11
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple14
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple15
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple8 triple7) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((triple8) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear is not red.
("bear" "is" "red" "-")
((((triple8 triple7) -> (rule6 % int2))) -> (rule3 % int1))
The bear is not red.
("bear" "is" "red" "-")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2