The bear does not need the cow. The bear sees the cow. The cow needs the bear. The cow needs the lion. The cow sees the lion. The cow visits the lion. The lion is nice. The lion is red. The lion is not rough. The lion is round. The lion is young. The lion needs the bear. The lion needs the cow. The lion sees the cow. The lion visits the bear. The lion visits the cow. If someone visits the cow then the cow does not visit the bear. If someone is young then they need the cow. If the lion does not need the cow then the lion does not need the bear. If someone needs the bear and they do not visit the cow then the cow sees the bear. If someone needs the lion then they do not visit the bear. If someone needs the cow and they do not need the bear then the bear is round. If the lion does not need the bear then the bear needs the lion. If someone sees the bear and the bear needs the cow then the bear needs the lion.
The bear does not need the cow.
("bear" "needs" "cow" "-")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone visits the cow then the cow does not visit the bear.
((("someone" "visits" "cow" "+")) -> ("cow" "visits" "bear" "-"))
If someone is young then they need the cow.
((("someone" "is" "young" "+")) -> ("someone" "needs" "cow" "+"))
If the lion does not need the cow then the lion does not need the bear.
((("lion" "needs" "cow" "~")) -> ("lion" "needs" "bear" "-"))
If someone needs the bear and they do not visit the cow then the cow sees the bear.
((("someone" "needs" "bear" "+") ("someone" "visits" "cow" "~")) -> ("cow" "sees" "bear" "+"))
If someone needs the lion then they do not visit the bear.
((("someone" "needs" "lion" "+")) -> ("someone" "visits" "bear" "-"))
If someone needs the cow and they do not need the bear then the bear is round.
((("someone" "needs" "cow" "+") ("someone" "needs" "bear" "~")) -> ("bear" "is" "round" "+"))
If the lion does not need the bear then the bear needs the lion.
((("lion" "needs" "bear" "~")) -> ("bear" "needs" "lion" "+"))
If someone sees the bear and the bear needs the cow then the bear needs the lion.
((("someone" "sees" "bear" "+") ("bear" "needs" "cow" "+")) -> ("bear" "needs" "lion" "+"))
The bear does not need the cow.
True
1
proof
[(triple1)]
("bear" "needs" "cow" "-")
triple1
The lion does not see the cow.
False
1
inv-proof
[(triple14)]
("lion" "sees" "cow" "-")
triple14
The cow does not visit the bear.
True
2
proof
[(((triple16) -> rule1) OR ((triple4) -> rule5))]
("cow" "visits" "bear" "-")
((triple16) -> (rule1 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
((triple4) -> (rule5 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
The cow visits the bear.
False
2
inv-proof
[(((triple16) -> rule1) OR ((triple4) -> rule5))]
("cow" "visits" "bear" "+")
((triple16) -> (rule1 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
((triple4) -> (rule5 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "round" "-")
The bear needs the lion.
Unknown
rconc
[@1: The bear needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "needs" "lion" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
@0: The bear does not need the cow.[(triple1)] The bear sees the cow.[(triple2)] The cow needs the bear.[(triple3)] The cow needs the lion.[(triple4)] The cow sees the lion.[(triple5)] The cow visits the lion.[(triple6)] The lion is nice.[(triple7)] The lion is not rough.[(triple9)] The lion is red.[(triple8)] The lion is round.[(triple10)] The lion is young.[(triple11)] The lion needs the bear.[(triple12)] The lion needs the cow.[(triple13 OR ((triple11) -> rule2))] The lion sees the cow.[(triple14)] The lion visits the bear.[(triple15)] The lion visits the cow.[(triple16)] @1: The cow does not visit the bear.[(((triple16) -> rule1) OR ((triple4) -> rule5))]
The bear does not need the cow.
("bear" "needs" "cow" "-")
triple1
The bear sees the cow.
("bear" "sees" "cow" "+")
triple2
The cow needs the bear.
("cow" "needs" "bear" "+")
triple3
The cow needs the lion.
("cow" "needs" "lion" "+")
triple4
The cow sees the lion.
("cow" "sees" "lion" "+")
triple5
The cow visits the lion.
("cow" "visits" "lion" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion is not rough.
("lion" "is" "rough" "-")
triple9
The lion is red.
("lion" "is" "red" "+")
triple8
The lion is round.
("lion" "is" "round" "+")
triple10
The lion is young.
("lion" "is" "young" "+")
triple11
The lion needs the bear.
("lion" "needs" "bear" "+")
triple12
The lion needs the cow.
("lion" "needs" "cow" "+")
triple13
((triple11) -> (rule2 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
triple14
The lion visits the bear.
("lion" "visits" "bear" "+")
triple15
The lion visits the cow.
("lion" "visits" "cow" "+")
triple16
The cow does not visit the bear.
("cow" "visits" "bear" "-")
((triple16) -> (rule1 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1
((triple4) -> (rule5 % int1))
The cow does not visit the bear.
("cow" "visits" "bear" "-")
int1