The bear sees the cow. The cow needs the dog. The cow sees the dog. The dog is kind. The dog likes the cow. The dog needs the bear. The dog sees the bear. The dog sees the cow. The dog sees the mouse. The mouse likes the cow. If something sees the bear then it needs the dog.
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
If something sees the bear then it needs the dog.
((("something" "sees" "bear" "+")) -> ("something" "needs" "dog" "+"))
The dog sees the cow.
True
1
proof
[(triple8)]
("dog" "sees" "cow" "+")
triple8
The cow does not see the dog.
False
1
inv-proof
[(triple3)]
("cow" "sees" "dog" "-")
triple3
The mouse does not need the dog.
Unknown
inv-rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "dog" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
@0: The bear sees the cow.[(triple1)] The cow needs the dog.[(triple2)] The cow sees the dog.[(triple3)] The dog is kind.[(triple4)] The dog likes the cow.[(triple5)] The dog needs the bear.[(triple6)] The dog sees the bear.[(triple7)] The dog sees the cow.[(triple8)] The dog sees the mouse.[(triple9)] The mouse likes the cow.[(triple10)] @1: The dog needs the dog.[(((triple7) -> rule1))]
The bear sees the cow.
("bear" "sees" "cow" "+")
triple1
The cow needs the dog.
("cow" "needs" "dog" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog likes the cow.
("dog" "likes" "cow" "+")
triple5
The dog needs the bear.
("dog" "needs" "bear" "+")
triple6
The dog sees the bear.
("dog" "sees" "bear" "+")
triple7
The dog sees the cow.
("dog" "sees" "cow" "+")
triple8
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple9
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple10
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple7) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1