The bear is green. The bear is nice. The bear needs the cow. The bear sees the cow. The bear sees the lion. The bear sees the mouse. The bear visits the lion. The cow needs the mouse. The cow visits the bear. The lion is green. The lion is nice. The lion visits the cow. The mouse is not big. The mouse is round. The mouse sees the lion. The mouse visits the bear. If something visits the lion and the lion sees the bear then it sees the bear. If something needs the cow then it needs the lion. If something needs the lion then it is big. If something needs the cow and the cow does not need the bear then the cow sees the bear. If the mouse sees the cow then the mouse needs the lion. If something visits the bear and it needs the bear then the bear does not visit the mouse.
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
If something visits the lion and the lion sees the bear then it sees the bear.
((("something" "visits" "lion" "+") ("lion" "sees" "bear" "+")) -> ("something" "sees" "bear" "+"))
If something needs the cow then it needs the lion.
((("something" "needs" "cow" "+")) -> ("something" "needs" "lion" "+"))
If something needs the lion then it is big.
((("something" "needs" "lion" "+")) -> ("something" "is" "big" "+"))
If something needs the cow and the cow does not need the bear then the cow sees the bear.
((("something" "needs" "cow" "+") ("cow" "needs" "bear" "~")) -> ("cow" "sees" "bear" "+"))
If the mouse sees the cow then the mouse needs the lion.
((("mouse" "sees" "cow" "+")) -> ("mouse" "needs" "lion" "+"))
If something visits the bear and it needs the bear then the bear does not visit the mouse.
((("something" "visits" "bear" "+") ("something" "needs" "bear" "+")) -> ("bear" "visits" "mouse" "-"))
The bear is nice.
True
1
proof
[(triple2)]
("bear" "is" "nice" "+")
triple2
The bear does not see the mouse.
False
1
inv-proof
[(triple6)]
("bear" "sees" "mouse" "-")
triple6
The bear needs the lion.
True
2
proof
[(((triple3) -> rule2))]
("bear" "needs" "lion" "+")
((triple3) -> (rule2 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "needs" "lion" "-")
((triple3) -> (rule2 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is big.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("bear" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is not big.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("bear" "is" "big" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The lion does not see the bear.
Unknown
inv-rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "bear" "-")
The cow is big.
Unknown
rconc
[@2: The cow is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cow" "is" "big" "+")
The mouse does not see the bear.
Unknown
inv-rconc
[@1: The mouse sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "bear" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
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 mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
@0: The bear is green.[(triple1)] The bear is nice.[(triple2)] The bear needs the cow.[(triple3)] The bear sees the cow.[(triple4)] The bear sees the lion.[(triple5)] The bear sees the mouse.[(triple6)] The bear visits the lion.[(triple7)] The cow needs the mouse.[(triple8)] The cow visits the bear.[(triple9)] The lion is green.[(triple10)] The lion is nice.[(triple11)] The lion visits the cow.[(triple12)] The mouse is not big.[(triple13)] The mouse is round.[(triple14)] The mouse sees the lion.[(triple15)] The mouse visits the bear.[(triple16)] @1: The bear needs the lion.[(((triple3) -> rule2))] @2: The bear is big.[(((((triple3) -> rule2)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear needs the cow.
("bear" "needs" "cow" "+")
triple3
The bear sees the cow.
("bear" "sees" "cow" "+")
triple4
The bear sees the lion.
("bear" "sees" "lion" "+")
triple5
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple6
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple8
The cow visits the bear.
("cow" "visits" "bear" "+")
triple9
The lion is green.
("lion" "is" "green" "+")
triple10
The lion is nice.
("lion" "is" "nice" "+")
triple11
The lion visits the cow.
("lion" "visits" "cow" "+")
triple12
The mouse is not big.
("mouse" "is" "big" "-")
triple13
The mouse is round.
("mouse" "is" "round" "+")
triple14
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple15
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple16
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple3) -> (rule2 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2