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