The bear is green. The bear is rough. The bear is round. The bear is young. The bear likes the cow. The bear does not see the cow. The bear does not visit the lion. The cow is not cold. The cow likes the bear. The cow sees the lion. The cow visits the lion. The lion is green. The lion is young. The lion does not like the bear. The lion sees the cow. The lion visits the cow. If something sees the cow and it likes the bear then the bear likes the lion. If something sees the lion then it sees the bear. If something sees the lion then it likes the lion.
The bear is green.
("bear" "is" "green" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear does not see the cow.
("bear" "sees" "cow" "-")
The bear does not visit the lion.
("bear" "visits" "lion" "-")
The cow is not cold.
("cow" "is" "cold" "-")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion does not like the bear.
("lion" "likes" "bear" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If something sees the cow and it likes the bear then the bear likes the lion.
((("something" "sees" "cow" "+") ("something" "likes" "bear" "+")) -> ("bear" "likes" "lion" "+"))
If something sees the lion then it sees the bear.
((("something" "sees" "lion" "+")) -> ("something" "sees" "bear" "+"))
If something sees the lion then it likes the lion.
((("something" "sees" "lion" "+")) -> ("something" "likes" "lion" "+"))
The lion sees the cow.
True
1
proof
[(triple15)]
("lion" "sees" "cow" "+")
triple15
The cow does not visit the lion.
False
1
inv-proof
[(triple11)]
("cow" "visits" "lion" "-")
triple11
The cow likes the lion.
True
2
proof
[(((triple10) -> rule3))]
("cow" "likes" "lion" "+")
((triple10) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow does not see the bear.
False
2
inv-proof
[(((triple10) -> rule2))]
("cow" "sees" "bear" "-")
((triple10) -> (rule2 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The bear does not like the lion.
Unknown
inv-rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "lion" "-")
The lion sees the bear.
Unknown
rconc
[@1: The lion sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "bear" "+")
The lion does not visit the bear.
Unknown
inv-random
[@0: The lion visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "bear" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The bear does not see the cow.[(triple6)] The bear does not visit the lion.[(triple7)] The bear is green.[(triple1)] The bear is rough.[(triple2)] The bear is round.[(triple3)] The bear is young.[(triple4)] The bear likes the cow.[(triple5)] The cow is not cold.[(triple8)] The cow likes the bear.[(triple9)] The cow sees the lion.[(triple10)] The cow visits the lion.[(triple11)] The lion does not like the bear.[(triple14)] The lion is green.[(triple12)] The lion is young.[(triple13)] The lion sees the cow.[(triple15)] The lion visits the cow.[(triple16)] @1: The cow likes the lion.[(((triple10) -> rule3))] The cow sees the bear.[(((triple10) -> rule2))]
The bear does not see the cow.
("bear" "sees" "cow" "-")
triple6
The bear does not visit the lion.
("bear" "visits" "lion" "-")
triple7
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear likes the cow.
("bear" "likes" "cow" "+")
triple5
The cow is not cold.
("cow" "is" "cold" "-")
triple8
The cow likes the bear.
("cow" "likes" "bear" "+")
triple9
The cow sees the lion.
("cow" "sees" "lion" "+")
triple10
The cow visits the lion.
("cow" "visits" "lion" "+")
triple11
The lion does not like the bear.
("lion" "likes" "bear" "-")
triple14
The lion is green.
("lion" "is" "green" "+")
triple12
The lion is young.
("lion" "is" "young" "+")
triple13
The lion sees the cow.
("lion" "sees" "cow" "+")
triple15
The lion visits the cow.
("lion" "visits" "cow" "+")
triple16
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple10) -> (rule3 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
((triple10) -> (rule2 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1