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